Bare Type Constructors and Variables

Methods

put :: BTyCon -> Put #

get :: Get BTyCon #

putList :: [BTyCon] -> Put #

NFData BTyCon Source #

Instance details

Methods

rnf :: BTyCon -> () #

Data BTyCon Source #

Instance details

Methods

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

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

toConstr :: BTyCon -> Constr #

dataTypeOf :: BTyCon -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic BTyCon Source #

Instance details

Associated Types

type Rep BTyCon

Instance details

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

Methods

from :: BTyCon -> Rep BTyCon x #

to :: Rep BTyCon x -> BTyCon #

Show BTyCon Source #

Instance details

Methods

showsPrec :: Int -> BTyCon -> ShowS #

show :: BTyCon -> String #

showList :: [BTyCon] -> ShowS #

Instance details

Methods

showsPrec :: Int -> BareSpec -> ShowS #

show :: BareSpec -> String #

showList :: [BareSpec] -> ShowS #

Eq BTyCon Source #

Instance details

Methods

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

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

Instance details

Methods

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

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

(>) :: DataDecl -> DataDecl -> Bool #

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

max :: DataDecl -> DataDecl -> DataDecl #

min :: DataDecl -> DataDecl -> DataDecl #

Ord BTyCon Source #

Instance details

Methods

compare :: BTyCon -> BTyCon -> Ordering #

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

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

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

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

max :: BTyCon -> BTyCon -> BTyCon #

min :: BTyCon -> BTyCon -> BTyCon #

Hashable BTyCon Source #

Instance details

Methods

hashWithSalt :: Int -> BTyCon -> Int #

hash :: BTyCon -> Int #

Fixpoint BTyCon Source #

Instance details

Methods

toFix :: BTyCon -> Doc #

simplify :: BTyCon -> BTyCon #

PPrint BTyCon Source #

Instance details

Methods

pprintTidy :: Tidy -> BTyCon -> Doc #

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

Loc BTyCon Source #

Instance details

Methods

srcSpan :: BTyCon -> SrcSpan #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl Source #

expand on a BareType actually applies the type- and expression- aliases.

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareType -> BareType Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source #

TyConable BTyCon Source #

Instance details

Methods

isFun :: BTyCon -> Bool Source #

isList :: BTyCon -> Bool Source #

isTuple :: BTyCon -> Bool Source #

ppTycon :: BTyCon -> Doc Source #

isClass :: BTyCon -> Bool Source #

isEmbeddedDict :: BTyCon -> Bool Source #

isEqual :: BTyCon -> Bool Source #

isOrdCls :: BTyCon -> Bool Source #

isEqCls :: BTyCon -> Bool Source #

isNumCls :: BTyCon -> Bool Source #

isFracCls :: BTyCon -> Bool Source #

FreeVar BTyCon BTyVar Source #

Instance details

Methods

freeVars :: BTyCon -> [BTyVar]

SubsTy BTyVar BSort BSort Source #

Instance details

Methods

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

SubsTy BTyVar BSort BTyCon Source #

Instance details

Methods

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

SubsTy Symbol Symbol (BRType r) Source #

Instance details

Methods

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

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #

Instance details

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #

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

Instance details

Methods

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

Expand (BRType ()) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BRType () -> BRType () Source #

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

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #

Reftable (RTProp BTyCon BTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar () -> Bool Source #

ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

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

Instance details

Methods

isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) Source #

type Rep BTyCon Source #

Instance details

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

mkBTyCon :: Located LHName -> BTyCon Source #

isClassBTyCon :: BTyCon -> Bool Source #

newtype BTyVar Source #

Constructors

BTV LocSymbol

Instances

Instances details

Binary BTyVar Source #

Instance details

Methods

put :: BTyVar -> Put #

get :: Get BTyVar #

putList :: [BTyVar] -> Put #

NFData BTyVar Source #

Instance details

Methods

rnf :: BTyVar -> () #

Data BTyVar Source #

Instance details

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 #

Generic BTyVar Source #

Instance details

Associated Types

type Rep BTyVar
Instance details Defined in Language.Haskell.Liquid.Types.RType type Rep BTyVar = D1 ('MetaData "BTyVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "BTV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol)))

Methods

from :: BTyVar -> Rep BTyVar x #

to :: Rep BTyVar x -> BTyVar #

Show BTyVar Source #

Instance details

Methods

showsPrec :: Int -> BTyVar -> ShowS #

show :: BTyVar -> String #

showList :: [BTyVar] -> ShowS #

Instance details

Methods

showsPrec :: Int -> BareSpec -> ShowS #

show :: BareSpec -> String #

showList :: [BareSpec] -> ShowS #

Eq BTyVar Source #

Instance details

Methods

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

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

Instance details

Methods

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

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

(>) :: DataDecl -> DataDecl -> Bool #

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

max :: DataDecl -> DataDecl -> DataDecl #

min :: DataDecl -> DataDecl -> DataDecl #

Ord BTyVar Source #

Instance details

Methods

compare :: BTyVar -> BTyVar -> Ordering #

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

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

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

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

max :: BTyVar -> BTyVar -> BTyVar #

min :: BTyVar -> BTyVar -> BTyVar #

Hashable BTyVar Source #

Instance details

Methods

hashWithSalt :: Int -> BTyVar -> Int #

hash :: BTyVar -> Int #

Symbolic BTyVar Source #

Instance details

Methods

symbol :: BTyVar -> Symbol #

PPrint BTyVar Source #

Instance details

Methods

pprintTidy :: Tidy -> BTyVar -> Doc #

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

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl Source #

expand on a BareType actually applies the type- and expression- aliases.

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareType -> BareType Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source #

FreeVar BTyCon BTyVar Source #

Instance details

Methods

freeVars :: BTyCon -> [BTyVar]

SubsTy BTyVar BSort BSort Source #

Instance details

Methods

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

SubsTy BTyVar BSort BTyCon Source #

Instance details

Methods

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

SubsTy Symbol Symbol (BRType r) Source #

Instance details

Methods

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

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #

Instance details

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #

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

Instance details

Methods

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

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

Instance details

Methods

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

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

Instance details

Methods

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

Expand (BRType ()) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BRType () -> BRType () Source #

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

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #

Reftable (RTProp BTyCon BTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar () -> Bool Source #

ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

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

Instance details

Methods

isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) Source #

type Rep BTyVar Source #

Instance details

type Rep BTyVar = D1 ('MetaData "BTyVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "BTV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol)))

Refined Type Constructors

data RTyCon Source #

Constructors

RTyCon TyCon ![RPVar] !TyConInfo

Instances

Instances details

NFData RTyCon Source #

Instance details

Methods

rnf :: RTyCon -> () #

Instance details

Methods

rnf :: REnv -> () #

Instance details

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Instance details

Methods

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

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

Data RTyCon Source #

Instance details

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 #

Instance details

Methods

Generic RTyCon Source #

Instance details

Associated Types

type Rep RTyCon

Instance details

type Rep RTyCon = D1 ('MetaData "RTyCon" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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))))

Methods

from :: RTyCon -> Rep RTyCon x #

to :: Rep RTyCon x -> RTyCon #

Show RTyCon Source #

Instance details

Methods

showsPrec :: Int -> RTyCon -> ShowS #

show :: RTyCon -> String #

showList :: [RTyCon] -> ShowS #

Instance details

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Eq RTyCon Source #

Instance details

Methods

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

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

Hashable RTyCon Source #

Instance details

Methods

hashWithSalt :: Int -> RTyCon -> Int #

hash :: RTyCon -> Int #

Symbolic RTyCon Source #

Instance details

Methods

symbol :: RTyCon -> Symbol #

Fixpoint RTyCon Source #

Instance details

Methods

toFix :: RTyCon -> Doc #

simplify :: RTyCon -> RTyCon #

PPrint RTyCon Source #

Instance details

Methods

pprintTidy :: Tidy -> RTyCon -> Doc #

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

Instance details

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

expand on a SpecType simply expands the refinements, i.e. *does not* apply the type aliases, but just the 1. predicate aliases, 2. inlines, 3. stuff from LogicMap

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> SpecType -> SpecType Source #

Instance details

Methods

(=*=) :: SpecType -> SpecType -> Bool Source #

TyConable RTyCon Source #

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

Instance details

Methods

isFun :: RTyCon -> Bool Source #

isList :: RTyCon -> Bool Source #

isTuple :: RTyCon -> Bool Source #

ppTycon :: RTyCon -> Doc Source #

isClass :: RTyCon -> Bool Source #

isEmbeddedDict :: RTyCon -> Bool Source #

isEqual :: RTyCon -> Bool Source #

isOrdCls :: RTyCon -> Bool Source #

isEqCls :: RTyCon -> Bool Source #

isNumCls :: RTyCon -> Bool Source #

isFracCls :: RTyCon -> Bool Source #

Instance details

Methods

FreeVar RTyCon RTyVar Source #

Instance details

Methods

freeVars :: RTyCon -> [RTyVar]

Instance details

Methods

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

SubsTy Symbol RSort Sort Source #

Instance details

Methods

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

SubsTy RTyVar RSort Sort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RSort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RTyCon Source #

Instance details

Methods

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

Instance details

Methods

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

Instance details

Methods

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

SubsTy tv RSort Predicate Source #

Instance details

Methods

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

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

Instance details

Methods

fresh :: m (RRType r) Source #

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

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

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

Instance details

Methods

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

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

Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #

Exception [Error] Source #

Instance details

Methods

PPrint (CtxError SpecType) Source #

Instance details

Methods

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

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

Instance details

Methods

syms :: RRProp Reft -> [Symbol] #

substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft #

substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft #

subst :: Subst -> RRProp Reft -> RRProp Reft #

subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft #

Result [Error] Source #

Instance details

Methods

Reftable (RTProp RTyCon RTyVar Reft) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar Reft -> Bool Source #

ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

toReft :: RTProp RTyCon RTyVar Reft -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar Reft Source #

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

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #

Reftable (RTProp RTyCon RTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar () -> Bool Source #

ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

(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

Methods

isTauto :: RType RTyCon RTyVar r -> Bool Source #

ppTy :: RType RTyCon RTyVar r -> Doc -> Doc Source #

top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

toReft :: RType RTyCon RTyVar r -> Reft Source #

ofReft :: Reft -> RType RTyCon RTyVar r Source #

type Rep RTyCon Source #

Instance details

type Rep RTyCon = D1 ('MetaData "RTyCon" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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 varianceTyArgs :: !VarianceInfo variance info for type variables variancePsArgs :: !VarianceInfo variance info for predicate variables sizeFunction :: !(Maybe SizeFun) logical UNARY function that computes the size of the structure

Instances

Instances details

NFData TyConInfo Source #

Instance details

Methods

rnf :: TyConInfo -> () #

Data TyConInfo Source #

Instance details

Methods

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

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

toConstr :: TyConInfo -> Constr #

dataTypeOf :: TyConInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic TyConInfo Source #

Instance details

Associated Types

type Rep TyConInfo

Instance details

type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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)))))

Methods

from :: TyConInfo -> Rep TyConInfo x #

to :: Rep TyConInfo x -> TyConInfo #

Show TyConInfo Source #

Instance details

Methods

showsPrec :: Int -> TyConInfo -> ShowS #

show :: TyConInfo -> String #

showList :: [TyConInfo] -> ShowS #

type Rep TyConInfo Source #

Instance details

type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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)))))

defaultTyConInfo :: TyConInfo Source #

rTyConPVs :: RTyCon -> [RPVar] Source #

isClassType :: TyConable c => RTypeV v c t t1 -> Bool Source #

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

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

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

Accessors for RTyCon

isEmbeddedClass :: TyConable c => RTypeV v c t t1 -> Bool Source #

Refinement Types

type RType c tv r = RTypeV Symbol c tv r Source #

data RTypeV v c tv r Source #

Constructors

RVar
Fields rt_var :: !tv rt_reft :: !r
RFun
Fields rt_bind :: !Symbol rt_rinfo :: !RFInfo rt_in :: !(RTypeV v c tv r) rt_out :: !(RTypeV v c tv r) rt_reft :: !r
RAllT
Fields rt_tvbind :: !(RTVUV v c tv) rt_ty :: !(RTypeV v c tv r) rt_ref :: !r
RAllP	"forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ (rt_pvbind)
Fields rt_pvbind :: !(PVUV v c tv) rt_ty :: !(RTypeV v c tv r)
RApp	For example, in [a]- v > h}>, we apply (via `RApp`) * the `RProp` denoted by `{h -> v > h}` to * the `RTyCon` denoted by `[]`.
Fields rt_tycon :: !c rt_args :: ![RTypeV v c tv r] rt_pargs :: ![RTPropV v c tv r] rt_reft :: !r
RAllE
Fields rt_bind :: !Symbol rt_allarg :: !(RTypeV v c tv r) rt_ty :: !(RTypeV v c tv r)
REx
Fields rt_bind :: !Symbol rt_exarg :: !(RTypeV v c tv r) rt_ty :: !(RTypeV v c tv r)
RExprArg (Located (ExprV v))	For expression arguments to type aliases see testsposvector2.hs
RAppTy
Fields rt_arg :: !(RTypeV v c tv r) rt_res :: !(RTypeV v c tv r) rt_reft :: !r
RRTy
Fields rt_env :: ![(Symbol, RTypeV v c tv r)] rt_ref :: !r rt_obl :: !Oblig rt_ty :: !(RTypeV v c tv r)
RHole r	let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs

Instances

Instances details

Instance details

Methods

rnf :: REnv -> () #

Instance details

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Instance details

Methods

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

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

Instance details

Methods

Instance details

Methods

showsPrec :: Int -> BareSpec -> ShowS #

show :: BareSpec -> String #

showList :: [BareSpec] -> ShowS #

Instance details

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Instance details

Methods

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

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

(>) :: DataDecl -> DataDecl -> Bool #

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

max :: DataDecl -> DataDecl -> DataDecl #

min :: DataDecl -> DataDecl -> DataDecl #

Instance details

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl Source #

expand on a BareType actually applies the type- and expression- aliases.

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareType -> BareType Source #

expand on a SpecType simply expands the refinements, i.e. *does not* apply the type aliases, but just the 1. predicate aliases, 2. inlines, 3. stuff from LogicMap

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> SpecType -> SpecType Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source #

Instance details

Methods

(=*=) :: SpecType -> SpecType -> Bool Source #

Instance details

Methods

Instance details

Methods

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

SubsTy Symbol RSort Sort Source #

Instance details

Methods

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

SubsTy BTyVar BSort BSort Source #

Instance details

Methods

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

SubsTy BTyVar BSort BTyCon Source #

Instance details

Methods

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

SubsTy RTyVar RSort Sort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RSort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RTyCon Source #

Instance details

Methods

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

Instance details

Methods

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

Instance details

Methods

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

SubsTy tv RSort Predicate Source #

Instance details

Methods

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

SubsTy Symbol Symbol (BRType r) Source #

Instance details

Methods

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

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #

Instance details

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #

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

Instance details

Methods

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

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

Instance details

Methods

fresh :: m (RRType r) Source #

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

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

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

Instance details

Methods

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

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

Instance details

Methods

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

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

Instance details

Methods

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

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

Instance details

Methods

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

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

Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #

Exception [Error] Source #

Instance details

Methods

PPrint (CtxError SpecType) Source #

Instance details

Methods

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

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

Instance details

Methods

syms :: RRProp Reft -> [Symbol] #

substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft #

substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft #

subst :: Subst -> RRProp Reft -> RRProp Reft #

subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft #

Expand (BRType ()) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BRType () -> BRType () Source #

Result [Error] Source #

Instance details

Methods

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

Instance details

Methods

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

show :: RTVU c tv -> String #

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

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

Instance details

Methods

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

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

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

Instance details

Methods

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

Functor (RTypeV v c tv) Source #

Instance details

Methods

fmap :: (a -> b) -> RTypeV v c tv a -> RTypeV v c tv b #

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

(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

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

Methods

mempty :: RType c tv r #

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

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

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

Instance details

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

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 #

Foldable (RTypeV v c tv) Source #

Instance details

Methods

fold :: Monoid m => RTypeV v c tv m -> m #

foldMap :: Monoid m => (a -> m) -> RTypeV v c tv a -> m #

foldMap' :: Monoid m => (a -> m) -> RTypeV v c tv a -> m #

foldr :: (a -> b -> b) -> b -> RTypeV v c tv a -> b #

foldr' :: (a -> b -> b) -> b -> RTypeV v c tv a -> b #

foldl :: (b -> a -> b) -> b -> RTypeV v c tv a -> b #

foldl' :: (b -> a -> b) -> b -> RTypeV v c tv a -> b #

foldr1 :: (a -> a -> a) -> RTypeV v c tv a -> a #

foldl1 :: (a -> a -> a) -> RTypeV v c tv a -> a #

toList :: RTypeV v c tv a -> [a] #

null :: RTypeV v c tv a -> Bool #

length :: RTypeV v c tv a -> Int #

elem :: Eq a => a -> RTypeV v c tv a -> Bool #

maximum :: Ord a => RTypeV v c tv a -> a #

minimum :: Ord a => RTypeV v c tv a -> a #

sum :: Num a => RTypeV v c tv a -> a #

product :: Num a => RTypeV v c tv a -> a #

Traversable (RTypeV v c tv) Source #

Instance details

Methods

traverse :: Applicative f => (a -> f b) -> RTypeV v c tv a -> f (RTypeV v c tv b) #

sequenceA :: Applicative f => RTypeV v c tv (f a) -> f (RTypeV v c tv a) #

mapM :: Monad m => (a -> m b) -> RTypeV v c tv a -> m (RTypeV v c tv b) #

sequence :: Monad m => RTypeV v c tv (m a) -> m (RTypeV v c tv a) #

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

Instance details

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

Methods

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

show :: RType c tv r -> String #

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

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

Instance details

Methods

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

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

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

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

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

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

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

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

Instance details

Defined in Language.Haskell.Liquid.Types.RTypeOp

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

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 BTyCon BTyVar (UReft Reft)) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #

Reftable (RTProp BTyCon BTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar () -> Bool Source #

ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

Reftable (RTProp RTyCon RTyVar Reft) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar Reft -> Bool Source #

ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

toReft :: RTProp RTyCon RTyVar Reft -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar Reft Source #

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

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #

Reftable (RTProp RTyCon RTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar () -> Bool Source #

ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

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

Instance details

Methods

isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) Source #

(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

Methods

isTauto :: RType RTyCon RTyVar r -> Bool Source #

ppTy :: RType RTyCon RTyVar r -> Doc -> Doc Source #

top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

toReft :: RType RTyCon RTyVar r -> Reft Source #

ofReft :: Reft -> RType RTyCon RTyVar r Source #

(Binary tv, Binary r, Binary c, Binary v) => Binary (RTypeV v c tv r) Source #

Instance details

Methods

put :: RTypeV v c tv r -> Put #

get :: Get (RTypeV v c tv r) #

putList :: [RTypeV v c tv r] -> Put #

(Data v, Data tv, Data c, Data r) => Data (RTypeV v c tv r) Source #

Instance details

Methods

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

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

toConstr :: RTypeV v c tv r -> Constr #

dataTypeOf :: RTypeV v c tv r -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RTypeV v c tv r) Source #

Instance details

Associated Types

type Rep (RTypeV v c tv r)
Instance details Defined in Language.Haskell.Liquid.Types.RType type Rep (RTypeV v c tv r)

Methods

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

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

(Eq tv, Eq v, Eq c, Eq r) => Eq (RTypeV v c tv r) Source #

Instance details

Methods

(==) :: RTypeV v c tv r -> RTypeV v c tv r -> Bool #

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

(Hashable tv, Hashable r, Hashable c, Hashable v) => Hashable (RTypeV v c tv r) Source #

Instance details

Methods

hashWithSalt :: Int -> RTypeV v c tv r -> Int #

hash :: RTypeV v c tv r -> Int #

type Rep (RTypeV v c tv r) Source #

Instance details

type Rep (RTypeV v 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 rf_args :: [(Symbol, τ)] arguments. e.g. `h` in the above example rf_body :: t Abstract refinement associated with `RTyCon`. e.g. `v > h` in the above example

Instances

Instances details

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #

Instance details

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #

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

Instance details

Methods

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

Functor (Ref τ) Source #

Instance details

Methods

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

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

Foldable (Ref τ) Source #

Instance details

Methods

fold :: Monoid m => Ref τ m -> m #

foldMap :: Monoid m => (a -> m) -> Ref τ a -> m #

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

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

foldr' :: (a -> b -> b) -> b -> Ref τ a -> b #

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

foldl' :: (b -> a -> b) -> b -> Ref τ a -> b #

foldr1 :: (a -> a -> a) -> Ref τ a -> a #

foldl1 :: (a -> a -> a) -> Ref τ a -> a #

toList :: Ref τ a -> [a] #

null :: Ref τ a -> Bool #

length :: Ref τ a -> Int #

elem :: Eq a => a -> Ref τ a -> Bool #

maximum :: Ord a => Ref τ a -> a #

minimum :: Ord a => Ref τ a -> a #

sum :: Num a => Ref τ a -> a #

product :: Num a => Ref τ a -> a #

Traversable (Ref τ) Source #

Instance details

Methods

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

sequenceA :: Applicative f => Ref τ (f a) -> f (Ref τ a) #

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

sequence :: Monad m => Ref τ (m a) -> m (Ref τ a) #

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

Instance details

Methods

syms :: RRProp Reft -> [Symbol] #

substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft #

substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft #

subst :: Subst -> RRProp Reft -> RRProp Reft #

subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft #

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

Instance details

Methods

put :: Ref τ t -> Put #

get :: Get (Ref τ t) #

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

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

Instance details

Methods

rnf :: Ref τ t -> () #

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

Instance details

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

Associated Types

type Rep (Ref τ t)

Instance details

type Rep (Ref τ t) = D1 ('MetaData "Ref" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RProp" 'PrefixI 'True) (S1 ('MetaSel ('Just "rf_args") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, τ)]) :*: S1 ('MetaSel ('Just "rf_body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

Methods

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

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

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

Instance details

Methods

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

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

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

Instance details

Methods

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

hash :: Ref τ t -> Int #

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

Instance details

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

Methods

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

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

Instance details

Methods

mempty :: RTProp c tv r #

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

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

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

Instance details

Methods

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

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

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

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

Instance details

Methods

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

show :: RTProp c tv r -> String #

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

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

Instance details

Defined in Language.Haskell.Liquid.Types.RTypeOp

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 BTyCon BTyVar (UReft Reft)) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #

Reftable (RTProp BTyCon BTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar () -> Bool Source #

ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source #

Reftable (RTProp RTyCon RTyVar Reft) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar Reft -> Bool Source #

ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

toReft :: RTProp RTyCon RTyVar Reft -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar Reft Source #

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

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #

Reftable (RTProp RTyCon RTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar () -> Bool Source #

ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

type Rep (Ref τ t) Source #

Instance details

type Rep (Ref τ t) = D1 ('MetaData "Ref" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RProp" 'PrefixI 'True) (S1 ('MetaSel ('Just "rf_args") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, τ)]) :*: S1 ('MetaSel ('Just "rf_body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

type RTProp c tv r = RTPropV Symbol 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.

type RTPropV v c tv r = Ref (RTypeV v c tv ()) (RTypeV v c tv r) Source #

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

newtype RTyVar Source #

Constructors

RTV TyVar

Instances

Instances details

NFData RTyVar Source #

Instance details

Methods

rnf :: RTyVar -> () #

Instance details

Methods

rnf :: REnv -> () #

Instance details

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Instance details

Methods

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

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

Data RTyVar Source #

Instance details

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 #

Instance details

Methods

Generic RTyVar Source #

Instance details

Associated Types

type Rep RTyVar
Instance details Defined in Language.Haskell.Liquid.Types.RType type Rep RTyVar = D1 ('MetaData "RTyVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "RTV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyVar)))

Methods

from :: RTyVar -> Rep RTyVar x #

to :: Rep RTyVar x -> RTyVar #

Show RTyVar Source #

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

Instance details

Methods

showsPrec :: Int -> RTyVar -> ShowS #

show :: RTyVar -> String #

showList :: [RTyVar] -> ShowS #

Instance details

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Eq RTyVar Source #

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

Instance details

Methods

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

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

Ord RTyVar Source #

Instance details

Methods

compare :: RTyVar -> RTyVar -> Ordering #

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

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

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

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

max :: RTyVar -> RTyVar -> RTyVar #

min :: RTyVar -> RTyVar -> RTyVar #

Hashable RTyVar Source #

Instance details

Methods

hashWithSalt :: Int -> RTyVar -> Int #

hash :: RTyVar -> Int #

Symbolic RTyVar Source #

Instance details

Methods

symbol :: RTyVar -> Symbol #

PPrint RTyVar Source #

Instance details

Methods

pprintTidy :: Tidy -> RTyVar -> Doc #

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

Instance details

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

expand on a SpecType simply expands the refinements, i.e. *does not* apply the type aliases, but just the 1. predicate aliases, 2. inlines, 3. stuff from LogicMap

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> SpecType -> SpecType Source #

Instance details

Methods

(=*=) :: SpecType -> SpecType -> Bool Source #

Instance details

Methods

FreeVar RTyCon RTyVar Source #

Instance details

Methods

freeVars :: RTyCon -> [RTyVar]

Instance details

Methods

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

SubsTy Symbol RSort Sort Source #

Instance details

Methods

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

SubsTy RTyVar RSort Sort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RSort Source #

Instance details

Methods

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

SubsTy RTyVar RSort RTyCon Source #

Instance details

Methods

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

Instance details

Methods

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

Instance details

Methods

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

SubsTy tv RSort Predicate Source #

Instance details

Methods

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

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

Instance details

Methods

fresh :: m (RRType r) Source #

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

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

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

Instance details

Methods

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

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

Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #

Exception [Error] Source #

Instance details

Methods

PPrint (CtxError SpecType) Source #

Instance details

Methods

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

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

Instance details

Methods

syms :: RRProp Reft -> [Symbol] #

substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft #

substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft #

subst :: Subst -> RRProp Reft -> RRProp Reft #

subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft #

Result [Error] Source #

Instance details

Methods

Reftable (RTProp RTyCon RTyVar Reft) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar Reft -> Bool Source #

ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

toReft :: RTProp RTyCon RTyVar Reft -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar Reft Source #

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

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #

Reftable (RTProp RTyCon RTyVar ()) Source #

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar () -> Bool Source #

ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source #

(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

Methods

isTauto :: RType RTyCon RTyVar r -> Bool Source #

ppTy :: RType RTyCon RTyVar r -> Doc -> Doc Source #

top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

toReft :: RType RTyCon RTyVar r -> Reft Source #

ofReft :: Reft -> RType RTyCon RTyVar r Source #

type Rep RTyVar Source #

Instance details

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

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 #

Classes describing operations on `RTypes`

class Eq c => TyConable c where Source #

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool Source #

isList :: c -> Bool Source #

isTuple :: c -> Bool Source #

ppTycon :: c -> Doc Source #

isClass :: c -> Bool Source #

isEmbeddedDict :: c -> Bool Source #

isEqual :: c -> Bool Source #

isOrdCls :: c -> Bool Source #

isEqCls :: c -> Bool Source #

isNumCls :: c -> Bool Source #

isFracCls :: c -> Bool Source #

Instances

Instances details

TyConable TyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: TyCon -> Bool Source # isList :: TyCon -> Bool Source # isTuple :: TyCon -> Bool Source # ppTycon :: TyCon -> Doc Source # isClass :: TyCon -> Bool Source # isEmbeddedDict :: TyCon -> Bool Source # isEqual :: TyCon -> Bool Source # isOrdCls :: TyCon -> Bool Source # isEqCls :: TyCon -> Bool Source # isNumCls :: TyCon -> Bool Source # isFracCls :: TyCon -> Bool Source #
TyConable LocSymbol Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: LocSymbol -> Bool Source # isList :: LocSymbol -> Bool Source # isTuple :: LocSymbol -> Bool Source # ppTycon :: LocSymbol -> Doc Source # isClass :: LocSymbol -> Bool Source # isEmbeddedDict :: LocSymbol -> Bool Source # isEqual :: LocSymbol -> Bool Source # isOrdCls :: LocSymbol -> Bool Source # isEqCls :: LocSymbol -> Bool Source # isNumCls :: LocSymbol -> Bool Source # isFracCls :: LocSymbol -> Bool Source #
TyConable Symbol Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: Symbol -> Bool Source # isList :: Symbol -> Bool Source # isTuple :: Symbol -> Bool Source # ppTycon :: Symbol -> Doc Source # isClass :: Symbol -> Bool Source # isEmbeddedDict :: Symbol -> Bool Source # isEqual :: Symbol -> Bool Source # isOrdCls :: Symbol -> Bool Source # isEqCls :: Symbol -> Bool Source # isNumCls :: Symbol -> Bool Source # isFracCls :: Symbol -> Bool Source #
TyConable BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: BTyCon -> Bool Source # isList :: BTyCon -> Bool Source # isTuple :: BTyCon -> Bool Source # ppTycon :: BTyCon -> Doc Source # isClass :: BTyCon -> Bool Source # isEmbeddedDict :: BTyCon -> Bool Source # isEqual :: BTyCon -> Bool Source # isOrdCls :: BTyCon -> Bool Source # isEqCls :: BTyCon -> Bool Source # isNumCls :: BTyCon -> Bool Source # isFracCls :: BTyCon -> Bool Source #
TyConable RTyCon Source #	TyConable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: RTyCon -> Bool Source # isList :: RTyCon -> Bool Source # isTuple :: RTyCon -> Bool Source # ppTycon :: RTyCon -> Doc Source # isClass :: RTyCon -> Bool Source # isEmbeddedDict :: RTyCon -> Bool Source # isEqual :: RTyCon -> Bool Source # isOrdCls :: RTyCon -> Bool Source # isEqCls :: RTyCon -> Bool Source # isNumCls :: RTyCon -> Bool Source # isFracCls :: RTyCon -> Bool Source #

Type Variables

data RTVar tv s Source #

Constructors

RTVar
Fields ty_var_value :: tv ty_var_info :: RTVInfo s

Instances

Instances details

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

Instance details

Methods

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

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

Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #

Functor (RTVar tv) Source #

Instance details

Methods

fmap :: (a -> b) -> RTVar tv a -> RTVar tv b #

(<$) :: a -> RTVar tv b -> RTVar tv a #

Foldable (RTVar tv) Source #

Instance details

Methods

fold :: Monoid m => RTVar tv m -> m #

foldMap :: Monoid m => (a -> m) -> RTVar tv a -> m #

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

foldr :: (a -> b -> b) -> b -> RTVar tv a -> b #

foldr' :: (a -> b -> b) -> b -> RTVar tv a -> b #

foldl :: (b -> a -> b) -> b -> RTVar tv a -> b #

foldl' :: (b -> a -> b) -> b -> RTVar tv a -> b #

foldr1 :: (a -> a -> a) -> RTVar tv a -> a #

foldl1 :: (a -> a -> a) -> RTVar tv a -> a #

toList :: RTVar tv a -> [a] #

null :: RTVar tv a -> Bool #

length :: RTVar tv a -> Int #

elem :: Eq a => a -> RTVar tv a -> Bool #

maximum :: Ord a => RTVar tv a -> a #

minimum :: Ord a => RTVar tv a -> a #

sum :: Num a => RTVar tv a -> a #

product :: Num a => RTVar tv a -> a #

Traversable (RTVar tv) Source #

Instance details

Methods

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

sequenceA :: Applicative f => RTVar tv (f a) -> f (RTVar tv a) #

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

sequence :: Monad m => RTVar tv (m a) -> m (RTVar tv a) #

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

Instance details

Methods

put :: RTVar tv s -> Put #

get :: Get (RTVar tv s) #

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

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

Instance details

Methods

rnf :: RTVar tv s -> () #

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

Instance details

Methods

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

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

toConstr :: RTVar tv s -> Constr #

dataTypeOf :: RTVar tv s -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RTVar tv s) Source #

Instance details

Associated Types

type Rep (RTVar tv s)

Instance details

type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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))))

Methods

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

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

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

Instance details

Methods

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

show :: RTVU c tv -> String #

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

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

Instance details

Methods

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

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

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

Instance details

Methods

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

hash :: RTVar tv s -> Int #

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

Instance details

Methods

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

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

type Rep (RTVar tv s) Source #

Instance details

type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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 rtv_is_pol :: Bool
RTVInfo
Fields rtv_name :: Symbol rtv_kind :: s rtv_is_val :: Bool rtv_is_pol :: Bool

Instances

Instances details

Functor RTVInfo Source #

Instance details

Methods

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

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

Foldable RTVInfo Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: RTVInfo a -> [a] #

null :: RTVInfo a -> Bool #

length :: RTVInfo a -> Int #

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

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

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

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

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

Traversable RTVInfo Source #

Instance details

Methods

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

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

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

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

Binary s => Binary (RTVInfo s) Source #

Instance details

Methods

put :: RTVInfo s -> Put #

get :: Get (RTVInfo s) #

putList :: [RTVInfo s] -> Put #

NFData s => NFData (RTVInfo s) Source #

Instance details

Methods

rnf :: RTVInfo s -> () #

Data s => Data (RTVInfo s) Source #

Instance details

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

Associated Types

type Rep (RTVInfo s)

Instance details

type Rep (RTVInfo s) = D1 ('MetaData "RTVInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RTVNoInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "RTVInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtv_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "rtv_kind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)) :*: (S1 ('MetaSel ('Just "rtv_is_val") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

Methods

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

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

Eq s => Eq (RTVInfo s) Source #

Instance details

Methods

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

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

Hashable s => Hashable (RTVInfo s) Source #

Instance details

Methods

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

hash :: RTVInfo s -> Int #

type Rep (RTVInfo s) Source #

Instance details

type Rep (RTVInfo s) = D1 ('MetaData "RTVInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RTVNoInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "RTVInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtv_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "rtv_kind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)) :*: (S1 ('MetaSel ('Just "rtv_is_val") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

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

type PVar t = PVarV Symbol t Source #

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

data PVarV v t Source #

Constructors

PV
Fields pname :: !Symbol ptype :: !t parg :: !Symbol pargs :: ![(t, Symbol, ExprV v)]

Instances

Instances details

Subable UsedPVar Source #

Instance details

Methods

syms :: UsedPVar -> [Symbol] #

substa :: (Symbol -> Symbol) -> UsedPVar -> UsedPVar #

substf :: (Symbol -> Expr) -> UsedPVar -> UsedPVar #

subst :: Subst -> UsedPVar -> UsedPVar #

subst1 :: UsedPVar -> (Symbol, Expr) -> UsedPVar #

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

Instance details

Methods

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

Functor (PVarV v) Source #

Instance details

Methods

fmap :: (a -> b) -> PVarV v a -> PVarV v b #

(<$) :: a -> PVarV v b -> PVarV v a #

PPrint (PVar a) Source #

Instance details

Methods

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

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

(Binary t, Binary v) => Binary (PVarV v t) Source #

Instance details

Methods

put :: PVarV v t -> Put #

get :: Get (PVarV v t) #

putList :: [PVarV v t] -> Put #

(NFData v, NFData t) => NFData (PVarV v t) Source #

Instance details

Methods

rnf :: PVarV v t -> () #

(Data v, Data t) => Data (PVarV v t) Source #

Instance details

Methods

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

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

toConstr :: PVarV v t -> Constr #

dataTypeOf :: PVarV v t -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (PVarV v t) Source #

Instance details

Associated Types

type Rep (PVarV v t)

Instance details

type Rep (PVarV v t) = D1 ('MetaData "PVarV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "PV" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ptype") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)) :*: (S1 ('MetaSel ('Just "parg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "pargs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(t, Symbol, ExprV v)]))))

Methods

from :: PVarV v t -> Rep (PVarV v t) x #

to :: Rep (PVarV v t) x -> PVarV v t #

(Show t, Show v, Fixpoint v, Ord v) => Show (PVarV v t) Source #

Instance details

Methods

showsPrec :: Int -> PVarV v t -> ShowS #

show :: PVarV v t -> String #

showList :: [PVarV v t] -> ShowS #

Eq (PVarV v t) Source #

Instance details

Methods

(==) :: PVarV v t -> PVarV v t -> Bool #

(/=) :: PVarV v t -> PVarV v t -> Bool #

Ord (PVarV v t) Source #

Instance details

Methods

compare :: PVarV v t -> PVarV v t -> Ordering #

(<) :: PVarV v t -> PVarV v t -> Bool #

(<=) :: PVarV v t -> PVarV v t -> Bool #

(>) :: PVarV v t -> PVarV v t -> Bool #

(>=) :: PVarV v t -> PVarV v t -> Bool #

max :: PVarV v t -> PVarV v t -> PVarV v t #

min :: PVarV v t -> PVarV v t -> PVarV v t #

Hashable (PVarV v a) Source #

Instance details

Methods

hashWithSalt :: Int -> PVarV v a -> Int #

hash :: PVarV v a -> Int #

type Rep (PVarV v t) Source #

Instance details

type Rep (PVarV v t) = D1 ('MetaData "PVarV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "PV" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ptype") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)) :*: (S1 ('MetaSel ('Just "parg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "pargs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(t, Symbol, ExprV v)]))))

pvType :: PVarV v t -> t Source #

type Predicate = PredicateV Symbol Source #

newtype PredicateV v Source #

Constructors

Pr [UsedPVarV v]

Instances

Instances details

NFData Predicate Source #

Instance details

Methods

rnf :: Predicate -> () #

Monoid Predicate Source #

Instance details

Methods

mempty :: Predicate #

mappend :: Predicate -> Predicate -> Predicate #

mconcat :: [Predicate] -> Predicate #

Semigroup Predicate Source #

Instance details

Methods

(<>) :: Predicate -> Predicate -> Predicate #

sconcat :: NonEmpty Predicate -> Predicate #

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

Show Predicate Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

showsPrec :: Int -> Predicate -> ShowS #

show :: Predicate -> String #

showList :: [Predicate] -> ShowS #

PPrint Predicate Source #

Instance details

Methods

pprintTidy :: Tidy -> Predicate -> Doc #

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

Subable Predicate Source #

Instance details

Methods

syms :: Predicate -> [Symbol] #

substa :: (Symbol -> Symbol) -> Predicate -> Predicate #

substf :: (Symbol -> Expr) -> Predicate -> Predicate #

subst :: Subst -> Predicate -> Predicate #

subst1 :: Predicate -> (Symbol, Expr) -> Predicate #

Reftable Predicate Source #

Instance details

Methods

isTauto :: Predicate -> Bool Source #

ppTy :: Predicate -> Doc -> Doc Source #

top :: Predicate -> Predicate Source #

meet :: Predicate -> Predicate -> Predicate Source #

toReft :: Predicate -> Reft Source #

ofReft :: Reft -> Predicate Source #

SubsTy tv RSort Predicate Source #

Instance details

Methods

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

Binary v => Binary (PredicateV v) Source #

Instance details

Methods

put :: PredicateV v -> Put #

get :: Get (PredicateV v) #

putList :: [PredicateV v] -> Put #

Data v => Data (PredicateV v) Source #

Instance details

Methods

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

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

toConstr :: PredicateV v -> Constr #

dataTypeOf :: PredicateV v -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (PredicateV v) Source #

Instance details

Associated Types

type Rep (PredicateV v)
Instance details Defined in Language.Haskell.Liquid.Types.RType type Rep (PredicateV v) = D1 ('MetaData "PredicateV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "Pr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UsedPVarV v])))

Methods

from :: PredicateV v -> Rep (PredicateV v) x #

to :: Rep (PredicateV v) x -> PredicateV v #

Ord v => Eq (PredicateV v) Source #

Instance details

Methods

(==) :: PredicateV v -> PredicateV v -> Bool #

(/=) :: PredicateV v -> PredicateV v -> Bool #

Ord v => Hashable (PredicateV v) Source #

Instance details

Methods

hashWithSalt :: Int -> PredicateV v -> Int #

hash :: PredicateV v -> Int #

type Rep (PredicateV v) Source #

Instance details

type Rep (PredicateV v) = D1 ('MetaData "PredicateV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "Pr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UsedPVarV v])))

Manipulating `Predicates`

emapExprVM :: Monad m => ([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v') Source #

A map traversal that collects the local variables in scope

mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v' Source #

emapPredicateVM :: Monad m => ([Symbol] -> v -> m v') -> PredicateV v -> m (PredicateV v') Source #

A map traversal that collects the local variables in scope

mapPVarV :: (v -> v') -> (t -> t') -> PVarV v t -> PVarV v' t' Source #

emapPVarVM :: Monad m => ([Symbol] -> v -> m v') -> ([Symbol] -> t -> m t') -> PVarV v t -> m (PVarV v' t') Source #

A map traversal that collects the local variables in scope

emapSubstVM :: Monad m => ([Symbol] -> v -> m v') -> SubstV v -> m (SubstV v') Source #

pvars :: Predicate -> [UsedPVar] Source #

pappSym :: Show a => a -> Symbol Source #

pApp :: Symbol -> [Expr] -> Expr Source #

Refinements

type UReft r = UReftV Symbol r Source #

data UReftV v r Source #

Constructors

MkUReft
Fields ur_reft :: !r ur_pred :: !(PredicateV v)

Instances

Instances details

Instance details

Methods

rnf :: REnv -> () #

Instance details

Methods

mempty :: REnv #

mappend :: REnv -> REnv -> REnv #

mconcat :: [REnv] -> REnv #

Instance details

Methods

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

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

Instance details

Methods

Instance details

Methods

showsPrec :: Int -> BareSpec -> ShowS #

show :: BareSpec -> String #

showList :: [BareSpec] -> ShowS #

Instance details

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Instance details

Methods

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

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

(>) :: DataDecl -> DataDecl -> Bool #

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

max :: DataDecl -> DataDecl -> DataDecl #

min :: DataDecl -> DataDecl -> DataDecl #

Instance details

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl Source #

expand on a BareType actually applies the type- and expression- aliases.

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareType -> BareType Source #

Expand RReft Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> RReft -> RReft Source #

expand on a SpecType simply expands the refinements, i.e. *does not* apply the type aliases, but just the 1. predicate aliases, 2. inlines, 3. stuff from LogicMap

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> SpecType -> SpecType Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source #

Instance details

Methods

(=*=) :: SpecType -> SpecType -> Bool Source #

Instance details

Methods

Freshable m Integer => Freshable m RReft Source #

Instance details

Methods

fresh :: m RReft Source #

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

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

Instance details

Methods

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

Instance details

Methods

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

Instance details

Methods

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

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

Instance details

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

Methods

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

NFData r => NFData (UReft r) Source #

Instance details

Methods

rnf :: UReft r -> () #

Functor (UReftV v) Source #

Instance details

Methods

fmap :: (a -> b) -> UReftV v a -> UReftV v b #

(<$) :: a -> UReftV v b -> UReftV v a #

Monoid a => Monoid (UReft a) Source #

Instance details

Methods

mempty :: UReft a #

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

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

Semigroup a => Semigroup (UReft a) Source #

Instance details

Methods

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

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

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

Foldable (UReftV v) Source #

Instance details

Methods

fold :: Monoid m => UReftV v m -> m #

foldMap :: Monoid m => (a -> m) -> UReftV v a -> m #

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

foldr :: (a -> b -> b) -> b -> UReftV v a -> b #

foldr' :: (a -> b -> b) -> b -> UReftV v a -> b #

foldl :: (b -> a -> b) -> b -> UReftV v a -> b #

foldl' :: (b -> a -> b) -> b -> UReftV v a -> b #

foldr1 :: (a -> a -> a) -> UReftV v a -> a #

foldl1 :: (a -> a -> a) -> UReftV v a -> a #

toList :: UReftV v a -> [a] #

null :: UReftV v a -> Bool #

length :: UReftV v a -> Int #

elem :: Eq a => a -> UReftV v a -> Bool #

maximum :: Ord a => UReftV v a -> a #

minimum :: Ord a => UReftV v a -> a #

sum :: Num a => UReftV v a -> a #

product :: Num a => UReftV v a -> a #

Traversable (UReftV v) Source #

Instance details

Methods

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

sequenceA :: Applicative f => UReftV v (f a) -> f (UReftV v a) #

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

sequence :: Monad m => UReftV v (m a) -> m (UReftV v a) #

Exception [Error] Source #

Instance details

Methods

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

Instance details

Methods

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

show :: UReft r -> String #

showList :: [UReft r] -> ShowS #

PPrint (CtxError SpecType) Source #

Instance details

Methods

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

Expression (UReft ()) Source #

Instance details

Methods

expr :: UReft () -> Expr #

Subable r => Subable (UReft r) Source #

Instance details

Methods

syms :: UReft r -> [Symbol] #

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

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

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

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

REq (UReft Reft) Source #

Instance details

Methods

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

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

Instance details

Methods

isTauto :: UReft r -> Bool Source #

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

top :: UReft r -> UReft r Source #

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

toReft :: UReft r -> Reft Source #

ofReft :: Reft -> UReft r Source #

UReftable (UReft Reft) Source #

Instance details

Methods

ofUReft :: UReft Reft -> UReft Reft Source #

Result [Error] Source #

Instance details

Methods

(Binary r, Binary v) => Binary (UReftV v r) Source #

Instance details

Methods

put :: UReftV v r -> Put #

get :: Get (UReftV v r) #

putList :: [UReftV v r] -> Put #

(Data v, Data r) => Data (UReftV v r) Source #

Instance details

Methods

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

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

toConstr :: UReftV v r -> Constr #

dataTypeOf :: UReftV v r -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (UReftV v r) Source #

Instance details

Associated Types

type Rep (UReftV v r)

Instance details

type Rep (UReftV v r) = D1 ('MetaData "UReftV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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 (PredicateV v))))

Methods

from :: UReftV v r -> Rep (UReftV v r) x #

to :: Rep (UReftV v r) x -> UReftV v r #

(Ord v, Eq r) => Eq (UReftV v r) Source #

Instance details

Methods

(==) :: UReftV v r -> UReftV v r -> Bool #

(/=) :: UReftV v r -> UReftV v r -> Bool #

(Ord v, Hashable r) => Hashable (UReftV v r) Source #

Instance details

Methods

hashWithSalt :: Int -> UReftV v r -> Int #

hash :: UReftV v r -> Int #

(PPrint (PredicateV v), Reftable (PredicateV v), PPrint r, Reftable r) => PPrint (UReftV v r) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> UReftV v r -> Doc #

pprintPrec :: Int -> Tidy -> UReftV v r -> Doc #

ToReftV r => ToReftV (UReftV v r) Source #

Instance details

Associated Types

type ReftVar (UReftV v r)
Instance details Defined in Language.Haskell.Liquid.Types.RType type ReftVar (UReftV v r) = ReftVar r

Methods

toReftV :: UReftV v r -> ReftV (ReftVar (UReftV v r)) Source #

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

Instance details

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #

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

Instance details

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source #

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #

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

Instance details

Methods

isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool Source #

ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source #

top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft Source #

ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) Source #

type Rep (UReftV v r) Source #

Instance details

type Rep (UReftV v r) = D1 ('MetaData "UReftV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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 (PredicateV v))))

type ReftVar (UReftV v r) Source #

Instance details

type ReftVar (UReftV v r) = ReftVar r

mapUReftV :: (v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r' Source #

emapUReftVM :: Monad m => ([Symbol] -> v -> m v') -> (r -> m r') -> UReftV v r -> m (UReftV v' r') Source #

Parse-time entities describing refined data types

type SizeFun = SizeFunV Symbol Source #

Termination expressions

data SizeFunV v Source #

Constructors

IdSizeFun	x -> F.EVar x
SymSizeFun (Located v)	x -> f x

Instances

Instances details

Functor SizeFunV Source #

Instance details

Methods

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

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

Foldable SizeFunV Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: SizeFunV a -> [a] #

null :: SizeFunV a -> Bool #

length :: SizeFunV a -> Int #

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

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

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

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

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

Traversable SizeFunV Source #

Instance details

Methods

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

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

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

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

Binary v => Binary (SizeFunV v) Source #

Instance details

Methods

put :: SizeFunV v -> Put #

get :: Get (SizeFunV v) #

putList :: [SizeFunV v] -> Put #

NFData v => NFData (SizeFunV v) Source #

Instance details

Methods

rnf :: SizeFunV v -> () #

Data v => Data (SizeFunV v) Source #

Instance details

Methods

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

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

toConstr :: SizeFunV v -> Constr #

dataTypeOf :: SizeFunV v -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (SizeFunV v) Source #

Instance details

Associated Types

type Rep (SizeFunV v)

Instance details

type Rep (SizeFunV v) = D1 ('MetaData "SizeFunV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "IdSizeFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SymSizeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located v))))

Methods

from :: SizeFunV v -> Rep (SizeFunV v) x #

to :: Rep (SizeFunV v) x -> SizeFunV v #

Show v => Show (SizeFunV v) Source #

Instance details

Methods

showsPrec :: Int -> SizeFunV v -> ShowS #

show :: SizeFunV v -> String #

showList :: [SizeFunV v] -> ShowS #

Eq v => Eq (SizeFunV v) Source #

Instance details

Methods

(==) :: SizeFunV v -> SizeFunV v -> Bool #

(/=) :: SizeFunV v -> SizeFunV v -> Bool #

Hashable v => Hashable (SizeFunV v) Source #

Instance details

Methods

hashWithSalt :: Int -> SizeFunV v -> Int #

hash :: SizeFunV v -> Int #

PPrint v => PPrint (SizeFunV v) Source #

Instance details

Methods

pprintTidy :: Tidy -> SizeFunV v -> Doc #

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

type Rep (SizeFunV v) Source #

Instance details

type Rep (SizeFunV v) = D1 ('MetaData "SizeFunV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "IdSizeFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SymSizeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located v))))

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

data TyConP Source #

Constructors

TyConP
Fields tcpLoc :: !SourcePos tcpCon :: !TyCon tcpFreeTyVarsTy :: ![RTyVar] tcpFreePredTy :: ![PVar RSort] tcpVarianceTs :: !VarianceInfo tcpVariancePs :: !VarianceInfo tcpSizeFun :: !(Maybe SizeFun)

Instances

Instances details

Data TyConP Source #

Instance details

Methods

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

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

toConstr :: TyConP -> Constr #

dataTypeOf :: TyConP -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic TyConP Source #

Instance details

Associated Types

type Rep TyConP

Instance details

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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))))))

Methods

from :: TyConP -> Rep TyConP x #

to :: Rep TyConP x -> TyConP #

Show TyConP Source #

Instance details

Methods

showsPrec :: Int -> TyConP -> ShowS #

show :: TyConP -> String #

showList :: [TyConP] -> ShowS #

PPrint TyConP Source #

Instance details

Methods

pprintTidy :: Tidy -> TyConP -> Doc #

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

Loc TyConP Source #

Instance details

Methods

srcSpan :: TyConP -> SrcSpan #

type Rep TyConP Source #

Instance details

type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" '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

= RTypeV Symbol RTyCon RTyVar

Resolved version

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

type BRType Source #

Arguments

= RTypeV Symbol BTyCon BTyVar

Bare parsed version

type BRProp r = BRPropV Symbol r Source #

type BRPropV v r = Ref (BSortV v) (BRTypeV v r) Source #

type BSort = BRType () Source #

type BSortV v = BRTypeV v () Source #

type BPVar = PVar BSort Source #

type RTVU c tv = RTVUV Symbol c tv Source #

Unified Representation of Refinement Types --------------------------------

type PVU c tv = PVUV Symbol c tv Source #

Instantiated RType

type BareType = BareTypeV Symbol Source #

type BareTypeLHName = BareTypeV LHName Source #

type BareTypeParsed = BareTypeV LocSymbol Source #

type BareTypeV v = BRTypeV v (RReftV v) Source #

type SpecType = RRType RReft Source #

type SpecProp = RRProp RReft Source #

type SpecRTVar = RTVar RTyVar RSort Source #

type LocBareType = Located BareType Source #

type LocBareTypeLHName = Located BareTypeLHName Source #

type LocBareTypeParsed = Located BareTypeParsed Source #

type LocSpecType = Located SpecType Source #

type RSort = RRType () Source #

type UsedPVar = UsedPVarV Symbol Source #

Predicates ----------------------------------------------------------------

type UsedPVarV v = PVarV v () Source #

type RPVar = PVar RSort Source #

type RReft = RReftV Symbol Source #

type RReftV v = UReftV v (ReftV v) Source #

Printer Configuration

data PPEnv Source #

Printer ----------------------------------------------------------------

Constructors

PP
Fields ppPs :: Bool print abstract-predicates ppTyVar :: Bool print the unique suffix for each tyvar ppShort :: Bool print the tycons without qualification ppDebug :: Bool gross with full info

Instances

Instances details

Show PPEnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods showsPrec :: Int -> PPEnv -> ShowS # show :: PPEnv -> String # showList :: [PPEnv] -> ShowS #

ppEnv :: PPEnv Source #

ppEnvShort :: PPEnv -> PPEnv Source #

Refined Function Info

newtype RFInfo Source #

Constructors

RFInfo
Fields permitTC :: Maybe Bool

Instances

Instances details

Binary RFInfo Source #

Instance details

Methods

put :: RFInfo -> Put #

get :: Get RFInfo #

putList :: [RFInfo] -> Put #

NFData RFInfo Source #

Instance details

Methods

rnf :: RFInfo -> () #

Data RFInfo Source #

Instance details

Methods

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

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

toConstr :: RFInfo -> Constr #

dataTypeOf :: RFInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic RFInfo Source #

Instance details

Associated Types

type Rep RFInfo
Instance details Defined in Language.Haskell.Liquid.Types.RType type Rep RFInfo = D1 ('MetaData "RFInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "RFInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "permitTC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool))))

Methods

from :: RFInfo -> Rep RFInfo x #

to :: Rep RFInfo x -> RFInfo #

Show RFInfo Source #

Instance details

Methods

showsPrec :: Int -> RFInfo -> ShowS #

show :: RFInfo -> String #

showList :: [RFInfo] -> ShowS #

Eq RFInfo Source #

Instance details

Methods

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

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

Hashable RFInfo Source #

Instance details

Methods

hashWithSalt :: Int -> RFInfo -> Int #

hash :: RFInfo -> Int #

type Rep RFInfo Source #

Instance details

type Rep RFInfo = D1 ('MetaData "RFInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "RFInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "permitTC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool))))

defRFInfo :: RFInfo Source #

mkRFInfo :: Config -> RFInfo Source #

classRFInfo :: Bool -> RFInfo Source #

Reftable/UReftable Instances

class (Monoid r, Subable r) => Reftable r where Source #

Minimal complete definition

isTauto, ppTy, toReft, ofReft

Methods

isTauto :: r -> Bool Source #

ppTy :: r -> Doc -> Doc Source #

top :: r -> r Source #

meet :: r -> r -> r Source #

toReft :: r -> Reft Source #

ofReft :: Reft -> r Source #

Instances

Instances details

Reftable Reft Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isTauto :: Reft -> Bool Source # ppTy :: Reft -> Doc -> Doc Source # top :: Reft -> Reft Source # meet :: Reft -> Reft -> Reft Source # toReft :: Reft -> Reft Source # ofReft :: Reft -> Reft Source #
Reftable Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isTauto :: Predicate -> Bool Source # ppTy :: Predicate -> Doc -> Doc Source # top :: Predicate -> Predicate Source # meet :: Predicate -> Predicate -> Predicate Source # toReft :: Predicate -> Reft Source # ofReft :: Reft -> Predicate Source #
Reftable () Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isTauto :: () -> Bool Source # ppTy :: () -> Doc -> Doc Source # top :: () -> () Source # meet :: () -> () -> () Source # toReft :: () -> Reft Source # ofReft :: Reft -> () Source #
(PPrint r, Reftable r) => Reftable (UReft r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods isTauto :: UReft r -> Bool Source # ppTy :: UReft r -> Doc -> Doc Source # top :: UReft r -> UReft r Source # meet :: UReft r -> UReft r -> UReft r Source # toReft :: UReft r -> Reft Source # ofReft :: Reft -> UReft r Source #
Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool Source # ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source # top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source # meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source # toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft Source # ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) Source #
Reftable (RTProp BTyCon BTyVar ()) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar () -> Bool Source # ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc Source # top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source # meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () Source # toReft :: RTProp BTyCon BTyVar () -> Reft Source # ofReft :: Reft -> RTProp BTyCon BTyVar () Source #
Reftable (RTProp RTyCon RTyVar Reft) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool Source # ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc Source # top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source # meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source # toReft :: RTProp RTyCon RTyVar Reft -> Reft Source # ofReft :: Reft -> RTProp RTyCon RTyVar Reft Source #
Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool Source # ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc Source # top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source # meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source # toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft Source # ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) Source #
Reftable (RTProp RTyCon RTyVar ()) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar () -> Bool Source # ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc Source # top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source # meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () Source # toReft :: RTProp RTyCon RTyVar () -> Reft Source # ofReft :: Reft -> RTProp RTyCon RTyVar () Source #
Reftable (RType BTyCon BTyVar (UReft Reft)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool Source # ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc Source # top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source # meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source # toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft Source # ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) Source #
(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 Methods isTauto :: RType RTyCon RTyVar r -> Bool Source # ppTy :: RType RTyCon RTyVar r -> Doc -> Doc Source # top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source # meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source # toReft :: RType RTyCon RTyVar r -> Reft Source # ofReft :: Reft -> RType RTyCon RTyVar r Source #

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.RType Methods ofUReft :: UReft Reft -> () Source #
UReftable (UReft Reft) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods ofUReft :: UReft Reft -> UReft Reft Source #

class ToReftV r where Source #

Associated Types

type ReftVar r Source #

Methods

toReftV :: r -> ReftV (ReftVar r) Source #

Instances

Instances details

ToReftV () Source #

Instance details

Associated Types

type ReftVar ()
Instance details Defined in Language.Haskell.Liquid.Types.RType type ReftVar () = Symbol

Methods

toReftV :: () -> ReftV (ReftVar ()) Source #

ToReftV (ReftV v) Source #

Instance details

Associated Types

type ReftVar (ReftV v)
Instance details Defined in Language.Haskell.Liquid.Types.RType type ReftVar (ReftV v) = v

Methods

toReftV :: ReftV v -> ReftV (ReftVar (ReftV v)) Source #

ToReftV r => ToReftV (UReftV v r) Source #

Instance details