Ghc Information

Methods

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

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

Foldable Located

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: Located a -> [a] #

null :: Located a -> Bool #

length :: Located a -> Int #

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

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

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

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

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

Traversable Located

Instance details

Methods

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

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

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

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

ParseableV LocSymbol Source #

Instance details

Defined in Language.Haskell.Liquid.Parse

Methods

parseV :: ParserV LocSymbol LocSymbol #

mkSu :: [(Symbol, ExprV LocSymbol)] -> SubstV LocSymbol #

vFromString :: Located String -> LocSymbol #

Expand BareDef Source #

Instance details

Methods

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

Expand BareMeasure Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure 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 #

FromJSON a => FromJSON (Located a)

Instance details

Methods

parseJSON :: Value -> Parser (Located a) #

parseJSONList :: Value -> Parser [Located a] #

omittedField :: Maybe (Located a) #

ToJSON a => ToJSON (Located a)

Instance details

Methods

toJSON :: Located a -> Value #

toEncoding :: Located a -> Encoding #

toJSONList :: [Located a] -> Value #

toEncodingList :: [Located a] -> Encoding #

omitField :: Located a -> Bool #

Binary a => Binary (Located a)

Instance details

Methods

put :: Located a -> Put #

get :: Get (Located a) #

putList :: [Located a] -> Put #

NFData a => NFData (Located a)

Instance details

Methods

rnf :: Located a -> () #

Data a => Data (Located a)

Instance details

Methods

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

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

toConstr :: Located a -> Constr #

dataTypeOf :: Located a -> DataType #

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

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

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

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

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

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

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

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

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

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

IsString a => IsString (Located a)

Instance details

Methods

fromString :: String -> Located a #

Generic (Located a)

Instance details

Associated Types

type Rep (Located a)

Instance details

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

Methods

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

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

Show a => Show (Located a)

Instance details

Methods

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

show :: Located a -> String #

showList :: [Located a] -> ShowS #

Eq a => Eq (Located a)

Instance details

Methods

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

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

Ord a => Ord (Located a)

Instance details

Methods

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

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

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

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

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

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

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

Hashable a => Hashable (Located a)

Instance details

Methods

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

hash :: Located a -> Int #

ToHornSMT a => ToHornSMT (Located a)

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Located a -> Doc #

Symbolic a => Symbolic (Located a)

Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol #

Fixpoint a => Fixpoint (Located a)

Instance details

Methods

toFix :: Located a -> Doc #

simplify :: Located a -> Located a #

PPrint a => PPrint (Located a)

Instance details

Methods

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

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

Expression a => Expression (Located a)

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr #

Subable a => Subable (Located a)

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

syms :: Located a -> [Symbol] #

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

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

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

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

Loc (Located a)

Instance details

Methods

srcSpan :: Located a -> SrcSpan #

Expand a => Expand (Located a) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> Located a -> Located a Source #

REq r => REq (Located r) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Equality

Methods

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

Store a => Store (Located a)

Instance details

Methods

size :: Size (Located a) #

poke :: Located a -> Poke () #

peek :: Peek (Located a) #

Expand a => Expand (LocSymbol, a) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> (LocSymbol, a) -> (LocSymbol, a) Source #

type Rep (Located a)

Instance details

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

dummyLoc :: a -> Located a #

Symbols

type LocSymbol = Located Symbol #

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

type LocText = Located Text #

Default unknown name

dummyName :: Symbol #

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

Refinement Types

data RTAlias x a Source #

Refinement Type Aliases

Constructors

RTA
Fields rtName :: Symbol name of the alias rtTArgs :: [x] type parameters rtVArgs :: [Symbol] value parameters rtBody :: a what the alias expands to , rtMod :: !ModName -- ^ module where alias was defined

Instances

Instances details

Expand BareRTAlias Source #

Instance details

Methods

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

Functor (RTAlias x) Source #

Instance details

Methods

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

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

Foldable (RTAlias x) Source #

Instance details

Methods

fold :: Monoid m => RTAlias x m -> m #

foldMap :: Monoid m => (a -> m) -> RTAlias x a -> m #

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

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

foldr' :: (a -> b -> b) -> b -> RTAlias x a -> b #

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

foldl' :: (b -> a -> b) -> b -> RTAlias x a -> b #

foldr1 :: (a -> a -> a) -> RTAlias x a -> a #

foldl1 :: (a -> a -> a) -> RTAlias x a -> a #

toList :: RTAlias x a -> [a] #

null :: RTAlias x a -> Bool #

length :: RTAlias x a -> Int #

elem :: Eq a => a -> RTAlias x a -> Bool #

maximum :: Ord a => RTAlias x a -> a #

minimum :: Ord a => RTAlias x a -> a #

sum :: Num a => RTAlias x a -> a #

product :: Num a => RTAlias x a -> a #

Traversable (RTAlias x) Source #

Instance details

Methods

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

sequenceA :: Applicative f => RTAlias x (f a) -> f (RTAlias x a) #

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

sequence :: Monad m => RTAlias x (m a) -> m (RTAlias x a) #

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

Instance details

Methods

put :: RTAlias x a -> Put #

get :: Get (RTAlias x a) #

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

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

Instance details

Methods

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

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

toConstr :: RTAlias x a -> Constr #

dataTypeOf :: RTAlias x a -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RTAlias x a) Source #

Instance details

Associated Types

type Rep (RTAlias x a)

Instance details

type Rep (RTAlias x a) = D1 ('MetaData "RTAlias" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RTA" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "rtTArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [x])) :*: (S1 ('MetaSel ('Just "rtVArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "rtBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

Methods

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

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

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

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

Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

show :: RTAlias tv ty -> String #

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

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

Instance details

Methods

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

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

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

Instance details

Methods

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

hash :: RTAlias x a -> Int #

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

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

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

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

Expand (RTAlias Symbol Expr) Source #

Instance details

Methods

expand :: BareRTEnv -> SourcePos -> RTAlias Symbol Expr -> RTAlias Symbol Expr Source #

type Rep (RTAlias x a) Source #

Instance details

type Rep (RTAlias x a) = D1 ('MetaData "RTAlias" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RTA" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "rtTArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [x])) :*: (S1 ('MetaSel ('Just "rtVArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "rtBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

lmapEAlias :: LMap -> Located (RTAlias Symbol Expr) 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 #

class SubsTy tv ty a where Source #

Methods

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

Instances

Instances details

SubsTy TyVar Type SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy Symbol RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort Source #
SubsTy BTyVar BSort BSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort Source #
SubsTy BTyVar BSort BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #
SubsTy RTyVar RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort RSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort Source #
SubsTy RTyVar RSort RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #
SubsTy RTyVar RSort SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RTyVar SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
SubsTy tv RSort Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy tv ty Symbol Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> Symbol -> Symbol Source #
SubsTy tv ty Sort => SubsTy tv ty Expr Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> Expr -> Expr Source #
SubsTy tv ty Expr => SubsTy tv ty Reft Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> Reft -> Reft Source #
SubsTy tv ty () Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> () -> () Source #
SubsTy Symbol Symbol (BRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #
SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> PVar ty -> PVar ty Source #
SubsTy tv ty r => SubsTy tv ty (UReft r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> UReft r -> UReft r Source #
(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> (a, b) -> (a, b) Source #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType 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 Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #
SubsTy BTyVar (RType c BTyVar ()) BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar Source #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #

Relational predicates

type RelExpr = RelExprV Symbol Source #

Relational predicates --------------------------------------------------

data RelExprV v Source #

Constructors

ERBasic (ExprV v)
ERChecked (ExprV v) (RelExprV v)
ERUnChecked (ExprV v) (RelExprV v)

Instances

Instances details

Functor RelExprV Source #

Instance details

Methods

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

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

Foldable RelExprV Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: RelExprV a -> [a] #

null :: RelExprV a -> Bool #

length :: RelExprV a -> Int #

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

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

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

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

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

Traversable RelExprV Source #

Instance details

Methods

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

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

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

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

PPrint RelExpr Source #

Instance details

Methods

pprintTidy :: Tidy -> RelExpr -> Doc #

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

Binary v => Binary (RelExprV v) Source #

Instance details

Methods

put :: RelExprV v -> Put #

get :: Get (RelExprV v) #

putList :: [RelExprV v] -> Put #

Data v => Data (RelExprV v) Source #

Instance details

Methods

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

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

toConstr :: RelExprV v -> Constr #

dataTypeOf :: RelExprV v -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RelExprV v) Source #

Instance details

Associated Types

type Rep (RelExprV v)

Instance details

type Rep (RelExprV v) = D1 ('MetaData "RelExprV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "ERBasic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "ERChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v))) :+: C1 ('MetaCons "ERUnChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v)))))

Methods

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

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

(Show v, Fixpoint v, Ord v) => Show (RelExprV v) Source #

Instance details

Methods

showsPrec :: Int -> RelExprV v -> ShowS #

show :: RelExprV v -> String #

showList :: [RelExprV v] -> ShowS #

Eq v => Eq (RelExprV v) Source #

Instance details

Methods

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

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

type Rep (RelExprV v) Source #

Instance details

type Rep (RelExprV v) = D1 ('MetaData "RelExprV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "ERBasic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "ERChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v))) :+: C1 ('MetaCons "ERUnChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v)))))

Pre-instantiated RType

type REnv = AREnv SpecType Source #

The type used during constraint generation, used also to define contexts for errors, hence in this file, and NOT in elsewhere. **DO NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings, shared across all constraints + local : few bindings, relevant to particular constraints

data AREnv t Source #

Constructors

REnv
Fields reGlobal :: HashMap Symbol t the "global" names for module reLocal :: HashMap Symbol t the "local" names for sub-exprs

Instances

Instances details

NFData REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
Functor AREnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> AREnv a -> AREnv b # (<$) :: a -> AREnv b -> AREnv a #
Monoid REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
Semigroup REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
PPrint t => PPrint (AREnv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> AREnv t -> Doc # pprintPrec :: Int -> Tidy -> AREnv t -> Doc #

???

data Oblig Source #

Different kinds of Check Obligations ------------------------------------

Constructors

OTerm	Obligation that proves termination
OInv	Obligation that proves invariants
OCons	Obligation that proves subtyping constraints

Instances

Instances details

Binary Oblig Source #

Instance details

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

NFData Oblig Source #

Instance details

Methods

rnf :: Oblig -> () #

Data Oblig Source #

Instance details

Methods

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

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

toConstr :: Oblig -> Constr #

dataTypeOf :: Oblig -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic Oblig Source #

Instance details

Associated Types

type Rep Oblig
Instance details Defined in Language.Haskell.Liquid.Types.Errors type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: Oblig -> Rep Oblig x #

to :: Rep Oblig x -> Oblig #

Show Oblig Source #

Instance details

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

Eq Oblig Source #

Instance details

Methods

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

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

Hashable Oblig Source #

Instance details

Methods

hashWithSalt :: Int -> Oblig -> Int #

hash :: Oblig -> Int #

PPrint Oblig Source #

Instance details

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

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

type Rep Oblig Source #

Instance details

type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type)))

ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source #

Inferred Annotations

newtype AnnInfo a Source #

Annotations -------------------------------------------------------

Constructors

AI (HashMap SrcSpan [(Maybe Text, a)])

Instances

Instances details

Functor AnnInfo Source #

Instance details

Methods

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

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

FromJSON a => FromJSON (AnnInfo a) Source #

Instance details

Methods

parseJSON :: Value -> Parser (AnnInfo a) #

parseJSONList :: Value -> Parser [AnnInfo a] #

omittedField :: Maybe (AnnInfo a) #

ToJSON a => ToJSON (AnnInfo a) Source #

Instance details

Methods

toJSON :: AnnInfo a -> Value #

toEncoding :: AnnInfo a -> Encoding #

toJSONList :: [AnnInfo a] -> Value #

toEncodingList :: [AnnInfo a] -> Encoding #

omitField :: AnnInfo a -> Bool #

NFData a => NFData (AnnInfo a) Source #

Instance details

Methods

rnf :: AnnInfo a -> () #

Monoid (AnnInfo a) Source #

Instance details

Methods

mempty :: AnnInfo a #

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

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

Semigroup (AnnInfo a) Source #

Instance details

Methods

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

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

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

Data a => Data (AnnInfo a) Source #

Instance details

Methods

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

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

toConstr :: AnnInfo a -> Constr #

dataTypeOf :: AnnInfo a -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (AnnInfo a) Source #

Instance details

Associated Types

type Rep (AnnInfo a)
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (AnnInfo a) = D1 ('MetaData "AnnInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "AI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SrcSpan [(Maybe Text, a)]))))

Methods

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

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

PPrint a => Show (AnnInfo a) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

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

show :: AnnInfo a -> String #

showList :: [AnnInfo a] -> ShowS #

PPrint a => PPrint (AnnInfo a) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

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

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

type Rep (AnnInfo a) Source #

Instance details

type Rep (AnnInfo a) = D1 ('MetaData "AnnInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "AI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SrcSpan [(Maybe Text, a)]))))

data Annot t Source #

Constructors

AnnUse t
AnnDef t
AnnRDf t
AnnLoc SrcSpan

Instances

Instances details

Functor Annot Source #

Instance details

Methods

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

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

NFData a => NFData (Annot a) Source #

Instance details

Methods

rnf :: Annot a -> () #

Data t => Data (Annot t) Source #

Instance details

Methods

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

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

toConstr :: Annot t -> Constr #

dataTypeOf :: Annot t -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (Annot t) Source #

Instance details

Associated Types

type Rep (Annot t)

Instance details

type Rep (Annot t) = D1 ('MetaData "Annot" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "AnnUse" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) :+: (C1 ('MetaCons "AnnRDf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnLoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan))))

Methods

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

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

PPrint t => PPrint (Annot t) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

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

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

type Rep (Annot t) Source #

Instance details

type Rep (Annot t) = D1 ('MetaData "Annot" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "AnnUse" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) :+: (C1 ('MetaCons "AnnRDf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "AnnLoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan))))

Hole Information

data HoleInfo i t Source #

Var Hole Info -----------------------------------------------------

Constructors

HoleInfo
Fields htype :: t hloc :: SrcSpan henv :: AREnv t info :: i

Instances

Instances details

Functor (HoleInfo i) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> HoleInfo i a -> HoleInfo i b # (<$) :: a -> HoleInfo i b -> HoleInfo i a #
PPrint t => PPrint (HoleInfo i t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HoleInfo i t -> Doc # pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #

Overall Output

data Output a Source #

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

Constructors

O
Fields o_vars :: Maybe [String] o_types :: !(AnnInfo a) o_templs :: !(AnnInfo a) o_bots :: ![SrcSpan] o_result :: ErrorResult

Instances

Instances details

Functor Output Source #

Instance details

Methods

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

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

FromJSON (Output Doc) Source #

Instance details

Methods

parseJSON :: Value -> Parser (Output Doc) #

parseJSONList :: Value -> Parser [Output Doc] #

omittedField :: Maybe (Output Doc) #

ToJSON (Output Doc) Source #

Instance details

Methods

toJSON :: Output Doc -> Value #

toEncoding :: Output Doc -> Encoding #

toJSONList :: [Output Doc] -> Value #

toEncodingList :: [Output Doc] -> Encoding #

omitField :: Output Doc -> Bool #

Monoid (Output a) Source #

Instance details

Methods

mempty :: Output a #

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

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

Semigroup (Output a) Source #

Instance details

Methods

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

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

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

Generic (Output a) Source #

Instance details

Associated Types

type Rep (Output a)

Instance details

type Rep (Output a) = D1 ('MetaData "Output" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "O" 'PrefixI 'True) ((S1 ('MetaSel ('Just "o_vars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [String])) :*: S1 ('MetaSel ('Just "o_types") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a))) :*: (S1 ('MetaSel ('Just "o_templs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a)) :*: (S1 ('MetaSel ('Just "o_bots") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]) :*: S1 ('MetaSel ('Just "o_result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErrorResult)))))

Methods

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

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

PPrint a => PPrint (Output a) Source #

Instance details

Methods

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

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

type Rep (Output a) Source #

Instance details

type Rep (Output a) = D1 ('MetaData "Output" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "O" 'PrefixI 'True) ((S1 ('MetaSel ('Just "o_vars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [String])) :*: S1 ('MetaSel ('Just "o_types") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a))) :*: (S1 ('MetaSel ('Just "o_templs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a)) :*: (S1 ('MetaSel ('Just "o_bots") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]) :*: S1 ('MetaSel ('Just "o_result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErrorResult)))))

Refinement Hole

hole :: ExprV v Source #

isHole :: Expr -> Bool Source #

hasHole :: Reftable r => r -> Bool Source #

Class for values that can be pretty printed

class PPrint a where #

Implement either pprintTidy or pprintPrec

Minimal complete definition

Nothing

Methods

pprintTidy :: Tidy -> a -> Doc #

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

Instances

Instances details

PPrint Class Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Class -> Doc # pprintPrec :: Int -> Tidy -> Class -> Doc #
PPrint DataCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #
PPrint Type Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Type -> Doc # pprintPrec :: Int -> Tidy -> Type -> Doc #
PPrint TyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> TyCon -> Doc # pprintPrec :: Int -> Tidy -> TyCon -> Doc #
PPrint Name Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Name -> Doc # pprintPrec :: Int -> Tidy -> Name -> Doc #
PPrint SourceError Source #	A whole bunch of PPrint instances follow ----------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> SourceError -> Doc # pprintPrec :: Int -> Tidy -> SourceError -> Doc #
PPrint SrcSpan Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> SrcSpan -> Doc # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #
PPrint TyThing Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> TyThing -> Doc # pprintPrec :: Int -> Tidy -> TyThing -> Doc #
PPrint Var Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Var -> Doc # pprintPrec :: Int -> Tidy -> Var -> Doc #
PPrint CVertex
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> CVertex -> Doc # pprintPrec :: Int -> Tidy -> CVertex -> Doc #
PPrint KVGraph
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> KVGraph -> Doc # pprintPrec :: Int -> Tidy -> KVGraph -> Doc #
PPrint Rank
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> Rank -> Doc # pprintPrec :: Int -> Tidy -> Rank -> Doc #
PPrint Pred
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Pred -> Doc # pprintPrec :: Int -> Tidy -> Pred -> Doc #
PPrint Tag
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Tag -> Doc # pprintPrec :: Int -> Tidy -> Tag -> Doc #
PPrint Command
Instance details Defined in Language.Fixpoint.Smt.Types Methods pprintTidy :: Tidy -> Command -> Doc # pprintPrec :: Int -> Tidy -> Command -> Doc #
PPrint Recur
Instance details Defined in Language.Fixpoint.Solver.Instantiate Methods pprintTidy :: Tidy -> Recur -> Doc # pprintPrec :: Int -> Tidy -> Recur -> Doc #
PPrint TermOrigin
Instance details Defined in Language.Fixpoint.Solver.Rewrite Methods pprintTidy :: Tidy -> TermOrigin -> Doc # pprintPrec :: Int -> Tidy -> TermOrigin -> Doc #
PPrint WorkItem
Instance details Defined in Language.Fixpoint.Solver.Worklist Methods pprintTidy :: Tidy -> WorkItem -> Doc # pprintPrec :: Int -> Tidy -> WorkItem -> Doc #
PPrint AxiomEnv
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> AxiomEnv -> Doc # pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc #
PPrint Equation
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Equation -> Doc # pprintPrec :: Int -> Tidy -> Equation -> Doc #
PPrint GFixSolution
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc #
PPrint QualParam
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualParam -> Doc # pprintPrec :: Int -> Tidy -> QualParam -> Doc #
PPrint QualPattern
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualPattern -> Doc # pprintPrec :: Int -> Tidy -> QualPattern -> Doc #
PPrint Rewrite
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Rewrite -> Doc # pprintPrec :: Int -> Tidy -> Rewrite -> Doc #
PPrint IBindEnv
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> IBindEnv -> Doc # pprintPrec :: Int -> Tidy -> IBindEnv -> Doc #
PPrint Packs
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> Packs -> Doc # pprintPrec :: Int -> Tidy -> Packs -> Doc #
PPrint Error
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint Error1
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error1 -> Doc # pprintPrec :: Int -> Tidy -> Error1 -> Doc #
PPrint Symbol
Instance details Defined in Language.Fixpoint.Types.Names Methods pprintTidy :: Tidy -> Symbol -> Doc # pprintPrec :: Int -> Tidy -> Symbol -> Doc #
PPrint DocTable
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> DocTable -> Doc # pprintPrec :: Int -> Tidy -> DocTable -> Doc #
PPrint Tidy Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Tidy -> Doc # pprintPrec :: Int -> Tidy -> Tidy -> Doc #
PPrint Bop
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Bop -> Doc # pprintPrec :: Int -> Tidy -> Bop -> Doc #
PPrint Brel
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc # pprintPrec :: Int -> Tidy -> Brel -> Doc #
PPrint Constant
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc # pprintPrec :: Int -> Tidy -> Constant -> Doc #
PPrint KVSub
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVSub -> Doc # pprintPrec :: Int -> Tidy -> KVSub -> Doc #
PPrint KVar
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc # pprintPrec :: Int -> Tidy -> KVar -> Doc #
PPrint SymConst
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc # pprintPrec :: Int -> Tidy -> SymConst -> Doc #
PPrint BIndex
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BIndex -> Doc # pprintPrec :: Int -> Tidy -> BIndex -> Doc #
PPrint BindPred
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BindPred -> Doc # pprintPrec :: Int -> Tidy -> BindPred -> Doc #
PPrint Cube
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> Cube -> Doc # pprintPrec :: Int -> Tidy -> Cube -> Doc #
PPrint EQual
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EQual -> Doc # pprintPrec :: Int -> Tidy -> EQual -> Doc #
PPrint EbindSol
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EbindSol -> Doc # pprintPrec :: Int -> Tidy -> EbindSol -> Doc #
PPrint KIndex
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> KIndex -> Doc # pprintPrec :: Int -> Tidy -> KIndex -> Doc #
PPrint QBind
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> QBind -> Doc # pprintPrec :: Int -> Tidy -> QBind -> Doc #
PPrint DataCtor
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
PPrint DataDecl
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
PPrint DataField
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataField -> Doc # pprintPrec :: Int -> Tidy -> DataField -> Doc #
PPrint FTycon
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> FTycon -> Doc # pprintPrec :: Int -> Tidy -> FTycon -> Doc #
PPrint Sort
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> Sort -> Doc # pprintPrec :: Int -> Tidy -> Sort -> Doc #
PPrint TCArgs
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> TCArgs -> Doc # pprintPrec :: Int -> Tidy -> TCArgs -> Doc #
PPrint SrcSpan
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SrcSpan -> Doc # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #
PPrint Templates
Instance details Defined in Language.Fixpoint.Types.Templates Methods pprintTidy :: Tidy -> Templates -> Doc # pprintPrec :: Int -> Tidy -> Templates -> Doc #
PPrint Sem
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> Sem -> Doc # pprintPrec :: Int -> Tidy -> Sem -> Doc #
PPrint SmtSort
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> SmtSort -> Doc # pprintPrec :: Int -> Tidy -> SmtSort -> Doc #
PPrint TheorySymbol
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> TheorySymbol -> Doc # pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc #
PPrint Trigger
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Trigger -> Doc # pprintPrec :: Int -> Tidy -> Trigger -> Doc #
PPrint Stats
Instance details Defined in Language.Fixpoint.Utils.Statistics Methods pprintTidy :: Tidy -> Stats -> Doc # pprintPrec :: Int -> Tidy -> Stats -> Doc #
PPrint CGEnv Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGEnv -> Doc # pprintPrec :: Int -> Tidy -> CGEnv -> Doc #
PPrint CGInfo Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGInfo -> Doc # pprintPrec :: Int -> Tidy -> CGInfo -> Doc #
PPrint SubC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> SubC -> Doc # pprintPrec :: Int -> Tidy -> SubC -> Doc #
PPrint WfC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> WfC -> Doc # pprintPrec :: Int -> Tidy -> WfC -> Doc #
PPrint Pattern Source #
Instance details Defined in Language.Haskell.Liquid.GHC.Resugar Methods pprintTidy :: Tidy -> Pattern -> Doc # pprintPrec :: Int -> Tidy -> Pattern -> Doc #
PPrint BPspec Source #
Instance details Defined in Language.Haskell.Liquid.Parse Methods pprintTidy :: Tidy -> BPspec -> Doc # pprintPrec :: Int -> Tidy -> BPspec -> Doc #
PPrint SpecType => PPrint DataConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataConP -> Doc # pprintPrec :: Int -> Tidy -> DataConP -> Doc #
PPrint DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataName -> Doc # pprintPrec :: Int -> Tidy -> DataName -> Doc #
PPrint HasDataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc #
PPrint Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> Oblig -> Doc # pprintPrec :: Int -> Tidy -> Oblig -> Doc #
PPrint ParseError Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> ParseError -> Doc # pprintPrec :: Int -> Tidy -> ParseError -> Doc #
PPrint UserError Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> UserError -> Doc # pprintPrec :: Int -> Tidy -> UserError -> Doc #
PPrint LHName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Names Methods pprintTidy :: Tidy -> LHName -> Doc # pprintPrec :: Int -> Tidy -> LHName -> Doc #
PPrint BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> BTyCon -> Doc # pprintPrec :: Int -> Tidy -> BTyCon -> Doc #
PPrint BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> BTyVar -> Doc # pprintPrec :: Int -> Tidy -> BTyVar -> Doc #
PPrint Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> Predicate -> Doc # pprintPrec :: Int -> Tidy -> Predicate -> Doc #
PPrint RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> RTyCon -> Doc # pprintPrec :: Int -> Tidy -> RTyCon -> Doc #
PPrint RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> RTyVar -> Doc # pprintPrec :: Int -> Tidy -> RTyVar -> Doc #
PPrint TyConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> TyConP -> Doc # pprintPrec :: Int -> Tidy -> TyConP -> Doc #
PPrint TargetInfo Source #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetInfo -> Doc # pprintPrec :: Int -> Tidy -> TargetInfo -> Doc #
PPrint TargetSpec Source #	Pretty Printing -----------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetSpec -> Doc # pprintPrec :: Int -> Tidy -> TargetSpec -> Doc #
PPrint Cinfo Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Cinfo -> Doc # pprintPrec :: Int -> Tidy -> Cinfo -> Doc #
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint KVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVKind -> Doc # pprintPrec :: Int -> Tidy -> KVKind -> Doc #
PPrint KVProf Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVProf -> Doc # pprintPrec :: Int -> Tidy -> KVProf -> Doc #
PPrint LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LogicMap -> Doc # pprintPrec :: Int -> Tidy -> LogicMap -> Doc #
PPrint ModName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> ModName -> Doc # pprintPrec :: Int -> Tidy -> ModName -> Doc #
PPrint RelExpr Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RelExpr -> Doc # pprintPrec :: Int -> Tidy -> RelExpr -> Doc #
PPrint Variance Source #
Instance details Defined in Language.Haskell.Liquid.Types.Variance Methods pprintTidy :: Tidy -> Variance -> Doc # pprintPrec :: Int -> Tidy -> Variance -> Doc #
PPrint Def Source #
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods pprintTidy :: Tidy -> Def -> Doc # pprintPrec :: Int -> Tidy -> Def -> Doc #
PPrint DiffCheck Source #
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods pprintTidy :: Tidy -> DiffCheck -> Doc # pprintPrec :: Int -> Tidy -> DiffCheck -> Doc #
PPrint Doc
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Doc -> Doc # pprintPrec :: Int -> Tidy -> Doc -> Doc #
PPrint Text
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Text -> Doc # pprintPrec :: Int -> Tidy -> Text -> Doc #
PPrint Integer
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Integer -> Doc # pprintPrec :: Int -> Tidy -> Integer -> Doc #
PPrint ()
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> () -> Doc # pprintPrec :: Int -> Tidy -> () -> Doc #
PPrint Bool
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Bool -> Doc # pprintPrec :: Int -> Tidy -> Bool -> Doc #
PPrint Char
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Char -> Doc # pprintPrec :: Int -> Tidy -> Char -> Doc #
PPrint Float
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Float -> Doc # pprintPrec :: Int -> Tidy -> Float -> Doc #
PPrint Int
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Int -> Doc # pprintPrec :: Int -> Tidy -> Int -> Doc #
PPrint (Bind Var) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Bind Var -> Doc # pprintPrec :: Int -> Tidy -> Bind Var -> Doc #
PPrint (Expr Var) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Expr Var -> Doc # pprintPrec :: Int -> Tidy -> Expr Var -> Doc #
PPrint (Elims a)
Instance details Defined in Language.Fixpoint.Graph.Deps Methods pprintTidy :: Tidy -> Elims a -> Doc # pprintPrec :: Int -> Tidy -> Elims a -> Doc #
PPrint (Bind a)
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Bind a -> Doc # pprintPrec :: Int -> Tidy -> Bind a -> Doc #
PPrint (Cstr a)
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Cstr a -> Doc # pprintPrec :: Int -> Tidy -> Cstr a -> Doc #
PPrint (Query a)
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Query a -> Doc # pprintPrec :: Int -> Tidy -> Query a -> Doc #
PPrint (Var a)
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Var a -> Doc # pprintPrec :: Int -> Tidy -> Var a -> Doc #
PPrint (Worklist a)
Instance details Defined in Language.Fixpoint.Solver.Worklist Methods pprintTidy :: Tidy -> Worklist a -> Doc # pprintPrec :: Int -> Tidy -> Worklist a -> Doc #
PPrint (QualifierV v)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualifierV v -> Doc # pprintPrec :: Int -> Tidy -> QualifierV v -> Doc #
Fixpoint a => PPrint (SimpC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> SimpC a -> Doc # pprintPrec :: Int -> Tidy -> SimpC a -> Doc #
Fixpoint a => PPrint (SubC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> SubC a -> Doc # pprintPrec :: Int -> Tidy -> SubC a -> Doc #
Fixpoint a => PPrint (WfC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> WfC a -> Doc # pprintPrec :: Int -> Tidy -> WfC a -> Doc #
PPrint a => PPrint (SEnv a)
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> SEnv a -> Doc # pprintPrec :: Int -> Tidy -> SEnv a -> Doc #
PPrint a => PPrint (SizedEnv a)
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> SizedEnv a -> Doc # pprintPrec :: Int -> Tidy -> SizedEnv a -> Doc #
Fixpoint a => PPrint (FixResult a)
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> FixResult a -> Doc # pprintPrec :: Int -> Tidy -> FixResult a -> Doc #
(Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v)
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> ExprV v -> Doc # pprintPrec :: Int -> Tidy -> ExprV v -> Doc #
(Ord v, Fixpoint v) => PPrint (SubstV v)
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SubstV v -> Doc # pprintPrec :: Int -> Tidy -> SubstV v -> Doc #
PPrint a => PPrint (TCEmb a)
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> TCEmb a -> Doc # pprintPrec :: Int -> Tidy -> TCEmb a -> Doc #
PPrint a => PPrint (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> Located a -> Doc # pprintPrec :: Int -> Tidy -> Located a -> Doc #
PPrint a => PPrint (Triggered a)
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Triggered a -> Doc # pprintPrec :: Int -> Tidy -> Triggered a -> Doc #
Show a => PPrint (Trie a)
Instance details Defined in Language.Fixpoint.Utils.Trie Methods pprintTidy :: Tidy -> Trie a -> Doc # pprintPrec :: Int -> Tidy -> Trie a -> Doc #
(Show v, PPrint v) => PPrint (PlugTV v) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods pprintTidy :: Tidy -> PlugTV v -> Doc # pprintPrec :: Int -> Tidy -> PlugTV v -> Doc #
PPrint a => PPrint (Template a) Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Template Methods pprintTidy :: Tidy -> Template a -> Doc # pprintPrec :: Int -> Tidy -> Template a -> Doc #
PPrint ty => PPrint (DataCtorP ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataCtorP ty -> Doc # pprintPrec :: Int -> Tidy -> DataCtorP ty -> Doc #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
PPrint (CtxError Doc) Source #	Pretty Printing Error Messages -------------------------------------------- Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError Doc -> Doc # pprintPrec :: Int -> Tidy -> CtxError Doc -> Doc #
PPrint (PVar a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> PVar a -> Doc # pprintPrec :: Int -> Tidy -> PVar a -> Doc #
PPrint v => PPrint (SizeFunV v) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> SizeFunV v -> Doc # pprintPrec :: Int -> Tidy -> SizeFunV v -> Doc #
PPrint t => PPrint (AREnv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> AREnv t -> Doc # pprintPrec :: Int -> Tidy -> AREnv t -> Doc #
PPrint a => PPrint (AnnInfo a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> AnnInfo a -> Doc # pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #
PPrint t => PPrint (Annot t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Annot t -> Doc # pprintPrec :: Int -> Tidy -> Annot t -> Doc #
(PPrint v, Ord v, Fixpoint v) => PPrint (BodyV v) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BodyV v -> Doc # pprintPrec :: Int -> Tidy -> BodyV v -> Doc #
PPrint t => PPrint (CMeasure t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> CMeasure t -> Doc # pprintPrec :: Int -> Tidy -> CMeasure t -> Doc #
(Ord v, Fixpoint v, PPrint v) => PPrint (LMapV v) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LMapV v -> Doc # pprintPrec :: Int -> Tidy -> LMapV v -> Doc #
PPrint a => PPrint (Output a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Output a -> Doc # pprintPrec :: Int -> Tidy -> Output a -> Doc #
PPrint t => PPrint (RClass t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RClass t -> Doc # pprintPrec :: Int -> Tidy -> RClass t -> Doc #
PPrint t => PPrint (RISig t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RISig t -> Doc # pprintPrec :: Int -> Tidy -> RISig t -> Doc #
PPrint t => PPrint (RInstance t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RInstance t -> Doc # pprintPrec :: Int -> Tidy -> RInstance t -> Doc #
(Ord a, PPrint a) => PPrint (HashSet a)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> HashSet a -> Doc # pprintPrec :: Int -> Tidy -> HashSet a -> Doc #
PPrint a => PPrint (Maybe a)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Maybe a -> Doc # pprintPrec :: Int -> Tidy -> Maybe a -> Doc #
PPrint a => PPrint [a]
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> [a] -> Doc # pprintPrec :: Int -> Tidy -> [a] -> Doc #
(PPrint a, PPrint b) => PPrint (Either a b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Either a b -> Doc # pprintPrec :: Int -> Tidy -> Either a b -> Doc #
(PPrint a, PPrint b) => PPrint (Sol a b)
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> Sol a b -> Doc # pprintPrec :: Int -> Tidy -> Sol a b -> Doc #
(PPrint e, PPrint t) => PPrint (Bound t e) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods pprintTidy :: Tidy -> Bound t e -> Doc # pprintPrec :: Int -> Tidy -> Bound t e -> Doc #
(PPrint lname, PPrint ty) => PPrint (DataDeclP lname ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataDeclP lname ty -> Doc # pprintPrec :: Int -> Tidy -> DataDeclP lname ty -> Doc #
PPrint v => PPrint (RTVar v s) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> RTVar v s -> Doc # pprintPrec :: Int -> Tidy -> RTVar v s -> Doc #
(PPrint r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc # pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #
(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 #
(Show lname, PPrint lname, Show ty, PPrint ty, PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => PPrint (Spec lname ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods pprintTidy :: Tidy -> Spec lname ty -> Doc # pprintPrec :: Int -> Tidy -> Spec lname ty -> Doc #
PPrint t => PPrint (HoleInfo i t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HoleInfo i t -> Doc # pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #
(PPrint t, PPrint a) => PPrint (MSpec t a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MSpec t a -> Doc # pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #
(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #
(PPrint tv, PPrint t) => PPrint (RTEnv tv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTEnv tv t -> Doc # pprintPrec :: Int -> Tidy -> RTEnv tv t -> Doc #
(Ord a, PPrint a, PPrint b) => PPrint (HashMap a b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> HashMap a b -> Doc # pprintPrec :: Int -> Tidy -> HashMap a b -> Doc #
(PPrint a, PPrint b) => PPrint (a, b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b) -> Doc # pprintPrec :: Int -> Tidy -> (a, b) -> Doc #
OkRT c tv r => PPrint (RType c tv r) Source #	Pretty Printing RefType ---------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RType c tv r -> Doc # pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #
(PPrint a, PPrint v, Ord v, Fixpoint v) => PPrint (DefV v t a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DefV v t a -> Doc # pprintPrec :: Int -> Tidy -> DefV v t a -> Doc #
(PPrint v, Ord v, Fixpoint v, PPrint t, PPrint a) => PPrint (MeasureV v t a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MeasureV v t a -> Doc # pprintPrec :: Int -> Tidy -> MeasureV v t a -> Doc #
(PPrint a, PPrint b, PPrint c) => PPrint (a, b, c)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c) -> Doc #
(PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d) -> Doc #
(PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d, e) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d, e) -> Doc #

pprint :: PPrint a => a -> Doc #

Top-level pretty printer

showpp :: PPrint a => a -> String #

Modules and Imports

data ModName Source #

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

Constructors

ModName !ModType !ModuleName

Instances

Instances details

Data ModName Source #

Instance details

Methods

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

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

toConstr :: ModName -> Constr #

dataTypeOf :: ModName -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic ModName Source #

Instance details

Associated Types

type Rep ModName

Instance details

type Rep ModName = D1 ('MetaData "ModName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModuleName)))

Methods

from :: ModName -> Rep ModName x #

to :: Rep ModName x -> ModName #

Show ModName Source #

Instance details

Methods

showsPrec :: Int -> ModName -> ShowS #

show :: ModName -> String #

showList :: [ModName] -> ShowS #

Eq ModName Source #

Instance details

Methods

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

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

Ord ModName Source #

Instance details

Methods

compare :: ModName -> ModName -> Ordering #

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

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

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

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

max :: ModName -> ModName -> ModName #

min :: ModName -> ModName -> ModName #

Hashable ModName Source #

Instance details

Methods

hashWithSalt :: Int -> ModName -> Int #

hash :: ModName -> Int #

Symbolic ModName Source #

Instance details

Methods

symbol :: ModName -> Symbol #

PPrint ModName Source #

Instance details

Methods

pprintTidy :: Tidy -> ModName -> Doc #

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

type Rep ModName Source #

Instance details

type Rep ModName = D1 ('MetaData "ModName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModuleName)))

data ModType Source #

Constructors

Target
SrcImport
SpecImport

Instances

Instances details

Data ModType Source #

Instance details

Methods

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

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

toConstr :: ModType -> Constr #

dataTypeOf :: ModType -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic ModType Source #

Instance details

Associated Types

type Rep ModType
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Target" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SrcImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpecImport" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: ModType -> Rep ModType x #

to :: Rep ModType x -> ModType #

Show ModType Source #

Instance details

Methods

showsPrec :: Int -> ModType -> ShowS #

show :: ModType -> String #

showList :: [ModType] -> ShowS #

Eq ModType Source #

Instance details

Methods

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

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

Ord ModType Source #

Instance details

Methods

compare :: ModType -> ModType -> Ordering #

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

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

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

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

max :: ModType -> ModType -> ModType #

min :: ModType -> ModType -> ModType #

Hashable ModType Source #

Instance details

Methods

hashWithSalt :: Int -> ModType -> Int #

hash :: ModType -> Int #

type Rep ModType Source #

Instance details

type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Target" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SrcImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpecImport" 'PrefixI 'False) (U1 :: Type -> Type)))

isSrcImport :: ModName -> Bool Source #

isSpecImport :: ModName -> Bool Source #

isTarget :: ModName -> Bool Source #

getModName :: ModName -> ModuleName Source #

getModString :: ModName -> String Source #

Refinement Type Aliases

data RTEnv tv t Source #

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

Constructors

RTE
Fields typeAliases :: HashMap Symbol (Located (RTAlias tv t)) exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))

Instances

Instances details

Monoid (RTEnv tv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: RTEnv tv t # mappend :: RTEnv tv t -> RTEnv tv t -> RTEnv tv t # mconcat :: [RTEnv tv t] -> RTEnv tv t #
Semigroup (RTEnv tv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: RTEnv tv t -> RTEnv tv t -> RTEnv tv t # sconcat :: NonEmpty (RTEnv tv t) -> RTEnv tv t # stimes :: Integral b => b -> RTEnv tv t -> RTEnv tv t #
(PPrint tv, PPrint t) => PPrint (RTEnv tv t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTEnv tv t -> Doc # pprintPrec :: Int -> Tidy -> RTEnv tv t -> Doc #

type BareRTEnv = RTEnv Symbol BareType Source #

type SpecRTEnv = RTEnv RTyVar SpecType Source #

type BareRTAlias = RTAlias Symbol BareType Source #

type SpecRTAlias = RTAlias RTyVar SpecType Source #

Diagnostics, Warnings, Errors and Error Messages

type Error = TError SpecType Source #

type ErrorResult = FixResult UserError Source #

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

data Warning Source #

Diagnostic info -----------------------------------------------------------

Instances

Instances details

Show Warning Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Warning -> ShowS # show :: Warning -> String # showList :: [Warning] -> ShowS #
Eq Warning Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Warning -> Warning -> Bool # (/=) :: Warning -> Warning -> Bool #

mkWarning :: SrcSpan -> Doc -> Warning Source #

data Diagnostics Source #

Instances

Instances details

Monoid Diagnostics Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: Diagnostics # mappend :: Diagnostics -> Diagnostics -> Diagnostics # mconcat :: [Diagnostics] -> Diagnostics #
Semigroup Diagnostics Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: Diagnostics -> Diagnostics -> Diagnostics # sconcat :: NonEmpty Diagnostics -> Diagnostics # stimes :: Integral b => b -> Diagnostics -> Diagnostics #
Eq Diagnostics Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Diagnostics -> Diagnostics -> Bool # (/=) :: Diagnostics -> Diagnostics -> Bool #

mkDiagnostics :: [Warning] -> [Error] -> Diagnostics Source #

emptyDiagnostics :: Diagnostics Source #

noErrors :: Diagnostics -> Bool Source #

allWarnings :: Diagnostics -> [Warning] Source #

allErrors :: Diagnostics -> [Error] Source #

printWarning :: Logger -> Warning -> IO () Source #

Printing Warnings ---------------------------------------------------------

Source information (associated with constraints)

data Cinfo Source #

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

Constructors

Ci
Fields ci_loc :: !SrcSpan ci_err :: !(Maybe Error) ci_var :: !(Maybe Var)

Instances

Instances details

NFData Cinfo Source #

Instance details

Methods

rnf :: Cinfo -> () #

Generic Cinfo Source #

Instance details

Associated Types

type Rep Cinfo

Instance details

type Rep Cinfo = D1 ('MetaData "Cinfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Ci" 'PrefixI 'True) (S1 ('MetaSel ('Just "ci_loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ci_err") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Error)) :*: S1 ('MetaSel ('Just "ci_var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Var)))))

Methods

from :: Cinfo -> Rep Cinfo x #

to :: Rep Cinfo x -> Cinfo #

Show Cinfo Source #

Instance details

Methods

showsPrec :: Int -> Cinfo -> ShowS #

show :: Cinfo -> String #

showList :: [Cinfo] -> ShowS #

Eq Cinfo Source #

Instance details

Methods

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

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

Fixpoint Cinfo Source #

Instance details

Methods

toFix :: Cinfo -> Doc #

simplify :: Cinfo -> Cinfo #

PPrint Cinfo Source #

Instance details

Methods

pprintTidy :: Tidy -> Cinfo -> Doc #

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

Loc Cinfo Source #

Instance details

Methods

srcSpan :: Cinfo -> SrcSpan #

Result (FixResult Cinfo) Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

result :: FixResult Cinfo -> FixResult UserError Source #

type Rep Cinfo Source #

Instance details

type Rep Cinfo = D1 ('MetaData "Cinfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Ci" 'PrefixI 'True) (S1 ('MetaSel ('Just "ci_loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ci_err") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Error)) :*: S1 ('MetaSel ('Just "ci_var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Var)))))

Measures

type Measure ty ctor = MeasureV Symbol ty ctor Source #

data MeasureV v ty ctor Source #

Constructors

M
Fields msName :: Located LHName msSort :: ty msEqns :: [DefV v ty ctor] msKind :: !MeasureKind msUnSorted :: !UnSortedExprs

Instances

Instances details

Expand BareMeasure Source #

Instance details

Methods

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

Bifunctor (MeasureV v) Source #

Instance details

Methods

bimap :: (a -> b) -> (c -> d) -> MeasureV v a c -> MeasureV v b d #

first :: (a -> b) -> MeasureV v a c -> MeasureV v b c #

second :: (b -> c) -> MeasureV v a b -> MeasureV v a c #

Functor (MeasureV v ty) Source #

Instance details

Methods

fmap :: (a -> b) -> MeasureV v ty a -> MeasureV v ty b #

(<$) :: a -> MeasureV v ty b -> MeasureV v ty a #

Subable (Measure ty ctor) Source #

Instance details

Methods

syms :: Measure ty ctor -> [Symbol] #

substa :: (Symbol -> Symbol) -> Measure ty ctor -> Measure ty ctor #

substf :: (Symbol -> Expr) -> Measure ty ctor -> Measure ty ctor #

subst :: Subst -> Measure ty ctor -> Measure ty ctor #

subst1 :: Measure ty ctor -> (Symbol, Expr) -> Measure ty ctor #

Loc (Measure a b) Source #

Instance details

Methods

srcSpan :: Measure a b -> SrcSpan #

(Binary ty, Binary ctor, Binary v) => Binary (MeasureV v ty ctor) Source #

Instance details

Methods

put :: MeasureV v ty ctor -> Put #

get :: Get (MeasureV v ty ctor) #

putList :: [MeasureV v ty ctor] -> Put #

(Data v, Data ctor, Data ty) => Data (MeasureV v ty ctor) Source #

Instance details

Methods

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

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

toConstr :: MeasureV v ty ctor -> Constr #

dataTypeOf :: MeasureV v ty ctor -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> MeasureV v ty ctor -> MeasureV v ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MeasureV v ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MeasureV v ty ctor -> r #

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> MeasureV v ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) #

Generic (MeasureV v ty ctor) Source #

Instance details

Associated Types

type Rep (MeasureV v ty ctor)

Instance details

type Rep (MeasureV v ty ctor) = D1 ('MetaData "MeasureV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :*: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefV v ty ctor]) :*: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :*: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs)))))

Methods

from :: MeasureV v ty ctor -> Rep (MeasureV v ty ctor) x #

to :: Rep (MeasureV v ty ctor) x -> MeasureV v ty ctor #

PPrint (MeasureV v t a) => Show (MeasureV v t a) Source #

Instance details

Methods

showsPrec :: Int -> MeasureV v t a -> ShowS #

show :: MeasureV v t a -> String #

showList :: [MeasureV v t a] -> ShowS #

(Eq ty, Eq ctor, Eq v) => Eq (MeasureV v ty ctor) Source #

Instance details

Methods

(==) :: MeasureV v ty ctor -> MeasureV v ty ctor -> Bool #

(/=) :: MeasureV v ty ctor -> MeasureV v ty ctor -> Bool #

(Hashable ty, Hashable ctor, Hashable v) => Hashable (MeasureV v ty ctor) Source #

Instance details

Methods

hashWithSalt :: Int -> MeasureV v ty ctor -> Int #

hash :: MeasureV v ty ctor -> Int #

(PPrint v, Ord v, Fixpoint v, PPrint t, PPrint a) => PPrint (MeasureV v t a) Source #

Instance details

Methods

pprintTidy :: Tidy -> MeasureV v t a -> Doc #

pprintPrec :: Int -> Tidy -> MeasureV v t a -> Doc #

type Rep (MeasureV v ty ctor) Source #

Instance details

type Rep (MeasureV v ty ctor) = D1 ('MetaData "MeasureV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :*: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefV v ty ctor]) :*: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :*: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs)))))

type UnSortedExprs = [UnSortedExpr] Source #

type UnSortedExpr = ([Symbol], Expr) Source #

data MeasureKind Source #

Constructors

MsReflect	due to `reflect foo`, used for opaque reflection
MsMeasure	due to `measure foo` with old-style (non-haskell) equations
MsLifted	due to `measure foo` with new-style haskell equations
MsClass	due to `class measure` definition
MsAbsMeasure	due to `measure foo` without equations c.f. testsposT1223.hs
MsSelector	due to selector-fields e.g. `data Foo = Foo { fld :: Int }`
MsChecker	due to checkers e.g. `is-F` for `data Foo = F ... \| G ...`

Instances

Instances details

Binary MeasureKind Source #

Instance details

Methods

put :: MeasureKind -> Put #

get :: Get MeasureKind #

putList :: [MeasureKind] -> Put #

Data MeasureKind Source #

Instance details

Methods

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

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

toConstr :: MeasureKind -> Constr #

dataTypeOf :: MeasureKind -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic MeasureKind Source #

Instance details

Associated Types

type Rep MeasureKind

Instance details

type Rep MeasureKind = D1 ('MetaData "MeasureKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "MsReflect" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MsMeasure" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsLifted" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MsClass" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsAbsMeasure" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MsSelector" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsChecker" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: MeasureKind -> Rep MeasureKind x #

to :: Rep MeasureKind x -> MeasureKind #

Show MeasureKind Source #

Instance details

Methods

showsPrec :: Int -> MeasureKind -> ShowS #

show :: MeasureKind -> String #

showList :: [MeasureKind] -> ShowS #

Eq MeasureKind Source #

Instance details

Methods

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

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

Ord MeasureKind Source #

Instance details

Methods

compare :: MeasureKind -> MeasureKind -> Ordering #

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

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

(>) :: MeasureKind -> MeasureKind -> Bool #

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

max :: MeasureKind -> MeasureKind -> MeasureKind #

min :: MeasureKind -> MeasureKind -> MeasureKind #

Hashable MeasureKind Source #

Instance details

Methods

hashWithSalt :: Int -> MeasureKind -> Int #

hash :: MeasureKind -> Int #

type Rep MeasureKind Source #

Instance details

type Rep MeasureKind = D1 ('MetaData "MeasureKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "MsReflect" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MsMeasure" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsLifted" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MsClass" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsAbsMeasure" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MsSelector" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsChecker" 'PrefixI 'False) (U1 :: Type -> Type))))

data CMeasure ty Source #

Constructors

CM
Fields cName :: Located LHName cSort :: ty

Instances

Instances details

Functor CMeasure Source #

Instance details

Methods

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

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

Data ty => Data (CMeasure ty) Source #

Instance details

Methods

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

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

toConstr :: CMeasure ty -> Constr #

dataTypeOf :: CMeasure ty -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (CMeasure ty) Source #

Instance details

Associated Types

type Rep (CMeasure ty)

Instance details

type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)))

Methods

from :: CMeasure ty -> Rep (CMeasure ty) x #

to :: Rep (CMeasure ty) x -> CMeasure ty #

PPrint (CMeasure t) => Show (CMeasure t) Source #

Instance details

Methods

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

show :: CMeasure t -> String #

showList :: [CMeasure t] -> ShowS #

PPrint t => PPrint (CMeasure t) Source #

Instance details

Methods

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

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

type Rep (CMeasure ty) Source #

Instance details

type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)))

type Def ty ctor = DefV Symbol ty ctor Source #

data DefV v ty ctor Source #

Constructors

Def
Fields measure :: Located LHName ctor :: ctor dsort :: Maybe ty binds :: [(Symbol, Maybe ty)] body :: BodyV v

Instances

Instances details

Expand BareDef Source #

Instance details

Methods

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

Bifunctor (DefV v) Source #

Instance details

Methods

bimap :: (a -> b) -> (c -> d) -> DefV v a c -> DefV v b d #

first :: (a -> b) -> DefV v a c -> DefV v b c #

second :: (b -> c) -> DefV v a b -> DefV v a c #

Functor (DefV v ty) Source #

Instance details

Methods

fmap :: (a -> b) -> DefV v ty a -> DefV v ty b #

(<$) :: a -> DefV v ty b -> DefV v ty a #

Subable (Def ty ctor) Source #

Instance details

Methods

syms :: Def ty ctor -> [Symbol] #

substa :: (Symbol -> Symbol) -> Def ty ctor -> Def ty ctor #

substf :: (Symbol -> Expr) -> Def ty ctor -> Def ty ctor #

subst :: Subst -> Def ty ctor -> Def ty ctor #

subst1 :: Def ty ctor -> (Symbol, Expr) -> Def ty ctor #

(Binary ctor, Binary ty, Binary v) => Binary (DefV v ty ctor) Source #

Instance details

Methods

put :: DefV v ty ctor -> Put #

get :: Get (DefV v ty ctor) #

putList :: [DefV v ty ctor] -> Put #

(Data v, Data ty, Data ctor) => Data (DefV v ty ctor) Source #

Instance details

Methods

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

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

toConstr :: DefV v ty ctor -> Constr #

dataTypeOf :: DefV v ty ctor -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> DefV v ty ctor -> DefV v ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefV v ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefV v ty ctor -> r #

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefV v ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) #

Generic (DefV v ty ctor) Source #

Instance details

Associated Types

type Rep (DefV v ty ctor)

Instance details

type Rep (DefV v ty ctor) = D1 ('MetaData "DefV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) ((S1 ('MetaSel ('Just "measure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "ctor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ctor)) :*: (S1 ('MetaSel ('Just "dsort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ty)) :*: (S1 ('MetaSel ('Just "binds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Maybe ty)]) :*: S1 ('MetaSel ('Just "body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BodyV v))))))

Methods

from :: DefV v ty ctor -> Rep (DefV v ty ctor) x #

to :: Rep (DefV v ty ctor) x -> DefV v ty ctor #

(Show ctor, Show ty, Show v, Fixpoint v, Ord v) => Show (DefV v ty ctor) Source #

Instance details

Methods

showsPrec :: Int -> DefV v ty ctor -> ShowS #

show :: DefV v ty ctor -> String #

showList :: [DefV v ty ctor] -> ShowS #

(Eq ctor, Eq ty, Eq v) => Eq (DefV v ty ctor) Source #

Instance details

Methods

(==) :: DefV v ty ctor -> DefV v ty ctor -> Bool #

(/=) :: DefV v ty ctor -> DefV v ty ctor -> Bool #

(Hashable ctor, Hashable ty, Hashable v) => Hashable (DefV v ty ctor) Source #

Instance details

Methods

hashWithSalt :: Int -> DefV v ty ctor -> Int #

hash :: DefV v ty ctor -> Int #

(PPrint a, PPrint v, Ord v, Fixpoint v) => PPrint (DefV v t a) Source #

Instance details

Methods

pprintTidy :: Tidy -> DefV v t a -> Doc #

pprintPrec :: Int -> Tidy -> DefV v t a -> Doc #

type Rep (DefV v ty ctor) Source #

Instance details

type Rep (DefV v ty ctor) = D1 ('MetaData "DefV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) ((S1 ('MetaSel ('Just "measure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "ctor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ctor)) :*: (S1 ('MetaSel ('Just "dsort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ty)) :*: (S1 ('MetaSel ('Just "binds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Maybe ty)]) :*: S1 ('MetaSel ('Just "body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BodyV v))))))

type Body = BodyV Symbol Source #

Measures

data BodyV v Source #

Constructors

E (ExprV v)	Measure Refinement: {v \| v = e }
P (ExprV v)	Measure Refinement: {v \| (? v) = p }
R Symbol (ExprV v)	Measure Refinement: {v \| p}

Instances

Instances details

Functor BodyV Source #

Instance details

Methods

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

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

Foldable BodyV Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: BodyV a -> [a] #

null :: BodyV a -> Bool #

length :: BodyV a -> Int #

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

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

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

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

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

Traversable BodyV Source #

Instance details

Methods

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

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

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

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

Subable Body Source #

Instance details

Methods

syms :: Body -> [Symbol] #

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

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

subst :: Subst -> Body -> Body #

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

Expand Body Source #

Instance details

Methods

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

Binary v => Binary (BodyV v) Source #

Instance details

Methods

put :: BodyV v -> Put #

get :: Get (BodyV v) #

putList :: [BodyV v] -> Put #

Data v => Data (BodyV v) Source #

Instance details

Methods

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

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

toConstr :: BodyV v -> Constr #

dataTypeOf :: BodyV v -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (BodyV v) Source #

Instance details

Associated Types

type Rep (BodyV v)

Instance details

type Rep (BodyV v) = D1 ('MetaData "BodyV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "E" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "P" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)))))

Methods

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

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

(Show v, Fixpoint v, Ord v) => Show (BodyV v) Source #

Instance details

Methods

showsPrec :: Int -> BodyV v -> ShowS #

show :: BodyV v -> String #

showList :: [BodyV v] -> ShowS #

Eq v => Eq (BodyV v) Source #

Instance details

Methods

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

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

Hashable v => Hashable (BodyV v) Source #

Instance details

Methods

hashWithSalt :: Int -> BodyV v -> Int #

hash :: BodyV v -> Int #

(PPrint v, Ord v, Fixpoint v) => PPrint (BodyV v) Source #

Instance details

Methods

pprintTidy :: Tidy -> BodyV v -> Doc #

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

type Rep (BodyV v) Source #

Instance details

type Rep (BodyV v) = D1 ('MetaData "BodyV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "E" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "P" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)))))

data MSpec ty ctor Source #

Constructors

MSpec
Fields ctorMap :: HashMap LHName [Def ty ctor] measMap :: HashMap (Located LHName) (Measure ty ctor) cmeasMap :: HashMap (Located LHName) (Measure ty ()) imeas :: ![Measure ty ctor]

Instances

Instances details

Bifunctor MSpec Source #

Instance details

Methods

bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d #

first :: (a -> b) -> MSpec a c -> MSpec b c #

second :: (b -> c) -> MSpec a b -> MSpec a c #

Functor (MSpec ty) Source #

Instance details

Methods

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

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

Eq ctor => Monoid (MSpec ty ctor) Source #

Instance details

Methods

mempty :: MSpec ty ctor #

mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

mconcat :: [MSpec ty ctor] -> MSpec ty ctor #

Eq ctor => Semigroup (MSpec ty ctor) Source #

Instance details

Methods

(<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor #

stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #

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

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) #

toConstr :: MSpec ty ctor -> Constr #

dataTypeOf :: MSpec ty ctor -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

Generic (MSpec ty ctor) Source #

Instance details

Associated Types

type Rep (MSpec ty ctor)

Instance details

type Rep (MSpec ty ctor) = D1 ('MetaData "MSpec" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "MSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctorMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LHName [Def ty ctor])) :*: S1 ('MetaSel ('Just "measMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ctor)))) :*: (S1 ('MetaSel ('Just "cmeasMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ()))) :*: S1 ('MetaSel ('Just "imeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ctor]))))

Methods

from :: MSpec ty ctor -> Rep (MSpec ty ctor) x #

to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #

(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source #

Instance details

Methods

showsPrec :: Int -> MSpec ty ctor -> ShowS #

show :: MSpec ty ctor -> String #

showList :: [MSpec ty ctor] -> ShowS #

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

Instance details

Methods

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

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

type Rep (MSpec ty ctor) Source #

Instance details

type Rep (MSpec ty ctor) = D1 ('MetaData "MSpec" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "MSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctorMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LHName [Def ty ctor])) :*: S1 ('MetaSel ('Just "measMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ctor)))) :*: (S1 ('MetaSel ('Just "cmeasMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ()))) :*: S1 ('MetaSel ('Just "imeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ctor]))))

mapDefTy :: (ty0 -> ty1) -> DefV v ty0 ctor -> DefV v ty1 ctor Source #

mapMeasureTy :: (ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor Source #

emapDefM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> DefV v0 ty0 ctor -> m (DefV v1 ty1 ctor) Source #

mapDefV :: (v -> v') -> DefV v ty ctor -> DefV v' ty ctor Source #

mapMeasureV :: (v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor Source #

emapMeasureM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> MeasureV v0 ty0 ctor -> m (MeasureV v1 ty1 ctor) Source #

emapRelExprV :: Monad m => ([Symbol] -> v0 -> m v1) -> RelExprV v0 -> m (RelExprV v1) Source #

Type Classes

data RClass ty Source #

Constructors

RClass
Fields rcName :: BTyCon rcSupers :: [ty] rcTyVars :: [BTyVar] rcMethods :: [(Located LHName, ty)]

Instances

Instances details

Functor RClass Source #

Instance details

Methods

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

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

Foldable RClass Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: RClass a -> [a] #

null :: RClass a -> Bool #

length :: RClass a -> Int #

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

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

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

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

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

Traversable RClass Source #

Instance details

Methods

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

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

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

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

Binary ty => Binary (RClass ty) Source #

Instance details

Methods

put :: RClass ty -> Put #

get :: Get (RClass ty) #

putList :: [RClass ty] -> Put #

Data ty => Data (RClass ty) Source #

Instance details

Methods

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

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

toConstr :: RClass ty -> Constr #

dataTypeOf :: RClass ty -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RClass ty) Source #

Instance details

Associated Types

type Rep (RClass ty)

Instance details

type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RClass" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rcName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "rcSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :*: (S1 ('MetaSel ('Just "rcTyVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [BTyVar]) :*: S1 ('MetaSel ('Just "rcMethods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Located LHName, ty)]))))

Methods

from :: RClass ty -> Rep (RClass ty) x #

to :: Rep (RClass ty) x -> RClass ty #

Show ty => Show (RClass ty) Source #

Instance details

Methods

showsPrec :: Int -> RClass ty -> ShowS #

show :: RClass ty -> String #

showList :: [RClass ty] -> ShowS #

Eq ty => Eq (RClass ty) Source #

Instance details

Methods

(==) :: RClass ty -> RClass ty -> Bool #

(/=) :: RClass ty -> RClass ty -> Bool #

Hashable ty => Hashable (RClass ty) Source #

Instance details

Methods

hashWithSalt :: Int -> RClass ty -> Int #

hash :: RClass ty -> Int #

PPrint t => PPrint (RClass t) Source #

Instance details

Methods

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

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

type Rep (RClass ty) Source #

Instance details

type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RClass" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rcName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "rcSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :*: (S1 ('MetaSel ('Just "rcTyVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [BTyVar]) :*: S1 ('MetaSel ('Just "rcMethods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Located LHName, ty)]))))

KV Profiling

data KVKind Source #

KVar Profile --------------------------------------------------------------

Constructors

RecBindE Var	Recursive binder `letrec x = ...`
NonRecBindE Var	Non recursive binder `let x = ...`
TypeInstE
PredInstE
LamE
CaseE Int	Int is the number of cases
LetE
ProjectE	Projecting out field of

Instances

Instances details

NFData KVKind Source #

Instance details

Methods

rnf :: KVKind -> () #

Data KVKind Source #

Instance details

Methods

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

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

toConstr :: KVKind -> Constr #

dataTypeOf :: KVKind -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic KVKind Source #

Instance details

Associated Types

type Rep KVKind

Instance details

type Rep KVKind = D1 ('MetaData "KVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (((C1 ('MetaCons "RecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)) :+: C1 ('MetaCons "NonRecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var))) :+: (C1 ('MetaCons "TypeInstE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PredInstE" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "LamE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CaseE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "LetE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjectE" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: KVKind -> Rep KVKind x #

to :: Rep KVKind x -> KVKind #

Show KVKind Source #

Instance details

Methods

showsPrec :: Int -> KVKind -> ShowS #

show :: KVKind -> String #

showList :: [KVKind] -> ShowS #

Eq KVKind Source #

Instance details

Methods

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

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

Ord KVKind Source #

Instance details

Methods

compare :: KVKind -> KVKind -> Ordering #

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

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

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

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

max :: KVKind -> KVKind -> KVKind #

min :: KVKind -> KVKind -> KVKind #

Hashable KVKind Source #

Instance details

Methods

hashWithSalt :: Int -> KVKind -> Int #

hash :: KVKind -> Int #

PPrint KVKind Source #

Instance details

Methods

pprintTidy :: Tidy -> KVKind -> Doc #

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

type Rep KVKind Source #

Instance details

type Rep KVKind = D1 ('MetaData "KVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (((C1 ('MetaCons "RecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)) :+: C1 ('MetaCons "NonRecBindE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var))) :+: (C1 ('MetaCons "TypeInstE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PredInstE" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "LamE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CaseE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "LetE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjectE" 'PrefixI 'False) (U1 :: Type -> Type))))

data KVProf Source #

Instances

Instances details

NFData KVProf Source #

Instance details

Methods

rnf :: KVProf -> () #

Generic KVProf Source #

Instance details

Associated Types

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

Methods

from :: KVProf -> Rep KVProf x #

to :: Rep KVProf x -> KVProf #

PPrint KVProf Source #

Instance details

Methods

pprintTidy :: Tidy -> KVProf -> Doc #

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

type Rep KVProf Source #

Instance details

type Rep KVProf = D1 ('MetaData "KVProf" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'True) (C1 ('MetaCons "KVP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap KVKind Int))))

emptyKVProf :: KVProf Source #

updKVProf :: KVKind -> Kuts -> KVProf -> KVProf Source #

Misc

mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty Source #

CoreToLogic

data LogicMap Source #

Constructors

LM
Fields lmSymDefs :: HashMap Symbol LMap Map from symbols to equations they define lmVarSyms :: HashMap Var (Maybe Symbol) Map from (lifted) Vars to `Symbol`; see: NOTE:LIFTED-VAR-SYMBOLS and NOTE:REFLECT-IMPORTs

Instances

Instances details

Monoid LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: LogicMap # mappend :: LogicMap -> LogicMap -> LogicMap # mconcat :: [LogicMap] -> LogicMap #
Semigroup LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: LogicMap -> LogicMap -> LogicMap # sconcat :: NonEmpty LogicMap -> LogicMap # stimes :: Integral b => b -> LogicMap -> LogicMap #
Show LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> LogicMap -> ShowS # show :: LogicMap -> String # showList :: [LogicMap] -> ShowS #
PPrint LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LogicMap -> Doc # pprintPrec :: Int -> Tidy -> LogicMap -> Doc #

toLMapV :: (Located LHName, ([Symbol], ExprV v)) -> (Located LHName, LMapV v) Source #

mkLogicMap :: HashMap Symbol LMap -> LogicMap Source #

toLogicMap :: [(LocSymbol, ([Symbol], Expr))] -> LogicMap Source #

eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr Source #

emapLMapM :: Monad m => ([Symbol] -> v0 -> m v1) -> LMapV v0 -> m (LMapV v1) Source #

data LMapV v Source #

Constructors

LMap
Fields lmVar :: LocSymbol lmArgs :: [Symbol] lmExpr :: ExprV v

Instances

Instances details

Functor LMapV Source #

Instance details

Methods

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

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

Binary v => Binary (LMapV v) Source #

Instance details

Methods

put :: LMapV v -> Put #

get :: Get (LMapV v) #

putList :: [LMapV v] -> Put #

Data v => Data (LMapV v) Source #

Instance details

Methods

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

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

toConstr :: LMapV v -> Constr #

dataTypeOf :: LMapV v -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (LMapV v) Source #

Instance details

Associated Types

type Rep (LMapV v)

Instance details

type Rep (LMapV v) = D1 ('MetaData "LMapV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "LMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: (S1 ('MetaSel ('Just "lmArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "lmExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)))))

Methods

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

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

(Show v, Ord v, Fixpoint v) => Show (LMapV v) Source #

Instance details

Methods

showsPrec :: Int -> LMapV v -> ShowS #

show :: LMapV v -> String #

showList :: [LMapV v] -> ShowS #

Eq v => Eq (LMapV v) Source #

Instance details

Methods

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

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

Hashable v => Hashable (LMapV v) Source #

Instance details

Methods

hashWithSalt :: Int -> LMapV v -> Int #

hash :: LMapV v -> Int #

(Ord v, Fixpoint v, PPrint v) => PPrint (LMapV v) Source #

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LMapV v -> Doc #

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

type Rep (LMapV v) Source #

Instance details

type Rep (LMapV v) = D1 ('MetaData "LMapV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "LMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: (S1 ('MetaSel ('Just "lmArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "lmExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)))))

type LMap = LMapV Symbol Source #

Refined Instances

type RDEnv = DEnv Var SpecType Source #

newtype DEnv x ty Source #

Constructors

DEnv (HashMap x (HashMap Symbol (RISig ty)))

Instances

Instances details

Functor (DEnv x) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> DEnv x a -> DEnv x b # (<$) :: a -> DEnv x b -> DEnv x a #
Hashable x => Monoid (DEnv x ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: DEnv x ty # mappend :: DEnv x ty -> DEnv x ty -> DEnv x ty # mconcat :: [DEnv x ty] -> DEnv x ty #
Hashable x => Semigroup (DEnv x ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: DEnv x ty -> DEnv x ty -> DEnv x ty # sconcat :: NonEmpty (DEnv x ty) -> DEnv x ty # stimes :: Integral b => b -> DEnv x ty -> DEnv x ty #
(Show x, Show ty) => Show (DEnv x ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DEnv x ty -> ShowS # show :: DEnv x ty -> String # showList :: [DEnv x ty] -> ShowS #

data RInstance t Source #

Refined Instances ---------------------------------------------------------

Constructors

RI
Fields riclass :: BTyCon riDictName :: Maybe (Located LHName) The name of the dictionary Provided when resolving names ritype :: [t] risigs :: [(Located LHName, RISig t)]

Instances

Instances details

Functor RInstance Source #

Instance details

Methods

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

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

Foldable RInstance Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: RInstance a -> [a] #

null :: RInstance a -> Bool #

length :: RInstance a -> Int #

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

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

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

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

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

Traversable RInstance Source #

Instance details

Methods

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

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

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

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

Binary t => Binary (RInstance t) Source #

Instance details

Methods

put :: RInstance t -> Put #

get :: Get (RInstance t) #

putList :: [RInstance t] -> Put #

Data t => Data (RInstance t) Source #

Instance details

Methods

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

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

toConstr :: RInstance t -> Constr #

dataTypeOf :: RInstance t -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RInstance t) Source #

Instance details

Associated Types

type Rep (RInstance t)

Instance details

type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RI" 'PrefixI 'True) ((S1 ('MetaSel ('Just "riclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "riDictName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located LHName)))) :*: (S1 ('MetaSel ('Just "ritype") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "risigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Located LHName, RISig t)]))))

Methods

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

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

Show t => Show (RInstance t) Source #

Instance details

Methods

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

show :: RInstance t -> String #

showList :: [RInstance t] -> ShowS #

Eq t => Eq (RInstance t) Source #

Instance details

Methods

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

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

Hashable t => Hashable (RInstance t) Source #

Instance details

Methods

hashWithSalt :: Int -> RInstance t -> Int #

hash :: RInstance t -> Int #

PPrint t => PPrint (RInstance t) Source #

Instance details

Methods

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

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

type Rep (RInstance t) Source #

Instance details

type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RI" 'PrefixI 'True) ((S1 ('MetaSel ('Just "riclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "riDictName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located LHName)))) :*: (S1 ('MetaSel ('Just "ritype") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "risigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Located LHName, RISig t)]))))

data RISig t Source #

Constructors

RIAssumed t
RISig t

Instances

Instances details

Functor RISig Source #

Instance details

Methods

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

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

Foldable RISig Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

toList :: RISig a -> [a] #

null :: RISig a -> Bool #

length :: RISig a -> Int #

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

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

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

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

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

Traversable RISig Source #

Instance details

Methods

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

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

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

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

Binary t => Binary (RISig t) Source #

Instance details

Methods

put :: RISig t -> Put #

get :: Get (RISig t) #

putList :: [RISig t] -> Put #

Data t => Data (RISig t) Source #

Instance details

Methods

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

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

toConstr :: RISig t -> Constr #

dataTypeOf :: RISig t -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic (RISig t) Source #

Instance details

Associated Types

type Rep (RISig t)

Instance details

type Rep (RISig t) = D1 ('MetaData "RISig" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) (C1 ('MetaCons "RIAssumed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "RISig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

Methods

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

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

Show t => Show (RISig t) Source #

Instance details

Methods

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

show :: RISig t -> String #

showList :: [RISig t] -> ShowS #

Eq t => Eq (RISig t) Source #

Instance details

Methods

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

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

Hashable t => Hashable (RISig t) Source #

Instance details

Methods

hashWithSalt :: Int -> RISig t -> Int #

hash :: RISig t -> Int #

PPrint t => PPrint (RISig t) Source #

Instance details

Methods

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

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

type Rep (RISig t) Source #

Instance details