Language.Haskell.Liquid.Types.Types

Core types

Ghc Information

data TyConMap

Information about Type Constructors

Constructors

TyConMap

Fields

• tcmTyRTy :: HashMap TyCon RTyCon

  Map from GHC TyCon to RTyCon

• tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon

  Map from GHC Family-Instances to RTyCon

• tcmFtcArity :: HashMap TyCon Int

  Arity of each Family-Tycon

Instances

Show TyConMap

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> TyConMap -> ShowS

show :: TyConMap -> String

showList :: [TyConMap] -> ShowS

F.Located Things

data Located a

Constructors

Loc

Fields

• loc :: !SourcePos

  Start Position

• locE :: !SourcePos

  End Position

• val :: !a

Instances

Functor Located

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

Foldable Located

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

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

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

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

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

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

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

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

toList :: Located a -> [a]

null :: Located a -> Bool

length :: Located a -> Int

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

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

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

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

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

Traversable Located

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

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

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

ParseableV LocSymbol

Defined in Language.Haskell.Liquid.Parse

Methods

parseV :: ParserV LocSymbol LocSymbol

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

vFromString :: Located String -> LocSymbol

Expand BareDef

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef

Expand BareMeasure

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure

TyConable LocSymbol

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: LocSymbol -> Bool

isList :: LocSymbol -> Bool

isTuple :: LocSymbol -> Bool

ppTycon :: LocSymbol -> Doc

isClass :: LocSymbol -> Bool

isEmbeddedDict :: LocSymbol -> Bool

isEqual :: LocSymbol -> Bool

isOrdCls :: LocSymbol -> Bool

isEqCls :: LocSymbol -> Bool

isNumCls :: LocSymbol -> Bool

isFracCls :: LocSymbol -> Bool

FromJSON a => FromJSON (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

parseJSON :: Value -> Parser (Located a)

parseJSONList :: Value -> Parser [Located a]

omittedField :: Maybe (Located a)

ToJSON a => ToJSON (Located a)

Defined in Language.Fixpoint.Types.Spans

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)

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Located a -> Put

get :: Get (Located a)

putList :: [Located a] -> Put

NFData a => NFData (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: Located a -> ()

Data a => Data (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

toConstr :: Located a -> Constr

dataTypeOf :: Located a -> DataType

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

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

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

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

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

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

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

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

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

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

IsString a => IsString (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

fromString :: String -> Located a

Generic (Located a)

Defined in Language.Fixpoint.Types.Spans

Associated Types

type Rep (Located a)

Defined in Language.Fixpoint.Types.Spans

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)

Defined in Language.Fixpoint.Types.Spans

Methods

showsPrec :: Int -> Located a -> ShowS

show :: Located a -> String

showList :: [Located a] -> ShowS

Eq a => Eq (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

Ord a => Ord (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

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

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

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

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

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

Hashable a => Hashable (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> Located a -> Int

hash :: Located a -> Int

ToHornSMT a => ToHornSMT (Located a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Located a -> Doc

Symbolic a => Symbolic (Located a)

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol

Fixpoint a => Fixpoint (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

toFix :: Located a -> Doc

simplify :: Located a -> Located a

PPrint a => PPrint (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> Located a -> Doc

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

Expression a => Expression (Located a)

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr

Subable a => Subable (Located a)

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)

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: Located a -> SrcSpan

Expand a => Expand (Located a)

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

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

REq r => REq (Located r)

Defined in Language.Haskell.Liquid.Types.Equality

Methods

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

Store a => Store (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

size :: Size (Located a)

poke :: Located a -> Poke ()

peek :: Peek (Located a)

Expand a => Expand (LocSymbol, a)

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

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

type Rep (Located a)

Defined in Language.Fixpoint.Types.Spans

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

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

Expand BareRTAlias

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias

Functor (RTAlias x)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable (RTAlias x)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RTAlias x a -> Put

get :: Get (RTAlias x a)

putList :: [RTAlias x a] -> Put

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: RTAlias x a -> Constr

dataTypeOf :: RTAlias x a -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (RTAlias x a)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RTAlias x a)

Defined in Language.Haskell.Liquid.Types.Types

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)

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

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

hash :: RTAlias x a -> Int

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

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)

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

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

type Rep (RTAlias x a)

Defined in Language.Haskell.Liquid.Types.Types

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)

Classes describing operations on RTypes

class Eq c => TyConable c where

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool

isList :: c -> Bool

isTuple :: c -> Bool

ppTycon :: c -> Doc

isClass :: c -> Bool

isEmbeddedDict :: c -> Bool

isEqual :: c -> Bool

isOrdCls :: c -> Bool

isEqCls :: c -> Bool

isNumCls :: c -> Bool

isFracCls :: c -> Bool

Instances

TyConable TyCon

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: TyCon -> Bool

isList :: TyCon -> Bool

isTuple :: TyCon -> Bool

ppTycon :: TyCon -> Doc

isClass :: TyCon -> Bool

isEmbeddedDict :: TyCon -> Bool

isEqual :: TyCon -> Bool

isOrdCls :: TyCon -> Bool

isEqCls :: TyCon -> Bool

isNumCls :: TyCon -> Bool

isFracCls :: TyCon -> Bool

TyConable LocSymbol

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: LocSymbol -> Bool

isList :: LocSymbol -> Bool

isTuple :: LocSymbol -> Bool

ppTycon :: LocSymbol -> Doc

isClass :: LocSymbol -> Bool

isEmbeddedDict :: LocSymbol -> Bool

isEqual :: LocSymbol -> Bool

isOrdCls :: LocSymbol -> Bool

isEqCls :: LocSymbol -> Bool

isNumCls :: LocSymbol -> Bool

isFracCls :: LocSymbol -> Bool

TyConable Symbol

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: Symbol -> Bool

isList :: Symbol -> Bool

isTuple :: Symbol -> Bool

ppTycon :: Symbol -> Doc

isClass :: Symbol -> Bool

isEmbeddedDict :: Symbol -> Bool

isEqual :: Symbol -> Bool

isOrdCls :: Symbol -> Bool

isEqCls :: Symbol -> Bool

isNumCls :: Symbol -> Bool

isFracCls :: Symbol -> Bool

TyConable BTyCon

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: BTyCon -> Bool

isList :: BTyCon -> Bool

isTuple :: BTyCon -> Bool

ppTycon :: BTyCon -> Doc

isClass :: BTyCon -> Bool

isEmbeddedDict :: BTyCon -> Bool

isEqual :: BTyCon -> Bool

isOrdCls :: BTyCon -> Bool

isEqCls :: BTyCon -> Bool

isNumCls :: BTyCon -> Bool

isFracCls :: BTyCon -> Bool

TyConable RTyCon

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

Defined in Language.Haskell.Liquid.Types.RType

Methods

isFun :: RTyCon -> Bool

isList :: RTyCon -> Bool

isTuple :: RTyCon -> Bool

ppTycon :: RTyCon -> Doc

isClass :: RTyCon -> Bool

isEmbeddedDict :: RTyCon -> Bool

isEqual :: RTyCon -> Bool

isOrdCls :: RTyCon -> Bool

isEqCls :: RTyCon -> Bool

isNumCls :: RTyCon -> Bool

isFracCls :: RTyCon -> Bool

class SubsTy tv ty a where

Methods

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

Instances

SubsTy TyVar Type SpecType

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy Symbol RSort Sort

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy BTyVar BSort BSort

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy BTyVar BSort BTyCon

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RSort Sort

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RSort RSort

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RSort RTyCon

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RSort SpecType

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar RTyVar SpecType

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv RSort Predicate

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv ty Symbol

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv ty Sort => SubsTy tv ty Expr

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv ty Expr => SubsTy tv ty Reft

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy tv ty ()

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy Symbol Symbol (BRType r)

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b)

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r)

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

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

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy BTyVar (RType c BTyVar ()) BTyVar

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ()))

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ()))

Defined in Language.Haskell.Liquid.Types.RefType

Methods

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

Relational predicates

type RelExpr = RelExprV Symbol

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

data RelExprV v

Constructors

ERBasic (ExprV v)

ERChecked (ExprV v) (RelExprV v)

ERUnChecked (ExprV v) (RelExprV v)

Instances

Functor RelExprV

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable RelExprV

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RelExpr -> Doc

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

Binary v => Binary (RelExprV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RelExprV v -> Put

get :: Get (RelExprV v)

putList :: [RelExprV v] -> Put

Data v => Data (RelExprV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RelExprV v)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RelExprV v -> ShowS

show :: RelExprV v -> String

showList :: [RelExprV v] -> ShowS

Eq v => Eq (RelExprV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

type Rep (RelExprV v)

Defined in Language.Haskell.Liquid.Types.Types

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

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

Constructors

REnv

Fields

• reGlobal :: HashMap Symbol t

  the "global" names for module

• reLocal :: HashMap Symbol t

  the "local" names for sub-exprs

Instances

NFData REnv

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: REnv -> ()

Functor AREnv

Defined in Language.Haskell.Liquid.Types.Types

Methods

fmap :: (a -> b) -> AREnv a -> AREnv b

(<$) :: a -> AREnv b -> AREnv a

Monoid REnv

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: REnv

mappend :: REnv -> REnv -> REnv

mconcat :: [REnv] -> REnv

Semigroup REnv

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> AREnv t -> Doc

pprintPrec :: Int -> Tidy -> AREnv t -> Doc

???

data Oblig

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

Constructors

OTerm

Obligation that proves termination

OInv

Obligation that proves invariants

OCons

Obligation that proves subtyping constraints

Instances

Binary Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

put :: Oblig -> Put

get :: Get Oblig

putList :: [Oblig] -> Put

NFData Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: Oblig -> ()

Data Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

toConstr :: Oblig -> Constr

dataTypeOf :: Oblig -> DataType

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

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

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

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

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

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

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

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

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

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

Generic Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Associated Types

type Rep Oblig

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

Defined in Language.Haskell.Liquid.Types.Errors

Methods

showsPrec :: Int -> Oblig -> ShowS

show :: Oblig -> String

showList :: [Oblig] -> ShowS

Eq Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

Hashable Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

hashWithSalt :: Int -> Oblig -> Int

hash :: Oblig -> Int

PPrint Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc

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

type Rep Oblig

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

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

Inferred Annotations

newtype AnnInfo a

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

Constructors

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

Instances

Functor AnnInfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

FromJSON a => FromJSON (AnnInfo a)

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

parseJSON :: Value -> Parser (AnnInfo a)

parseJSONList :: Value -> Parser [AnnInfo a]

omittedField :: Maybe (AnnInfo a)

ToJSON a => ToJSON (AnnInfo a)

Defined in Language.Haskell.Liquid.UX.DiffCheck

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: AnnInfo a -> ()

Monoid (AnnInfo a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: AnnInfo a

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

mconcat :: [AnnInfo a] -> AnnInfo a

Semigroup (AnnInfo a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

Data a => Data (AnnInfo a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: AnnInfo a -> Constr

dataTypeOf :: AnnInfo a -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (AnnInfo a)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (AnnInfo a)

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)

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)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> AnnInfo a -> Doc

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

type Rep (AnnInfo a)

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

data Annot t

Constructors

AnnUse t

AnnDef t

AnnRDf t

AnnLoc SrcSpan

Instances

Functor Annot

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

NFData a => NFData (Annot a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Annot a -> ()

Data t => Data (Annot t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: Annot t -> Constr

dataTypeOf :: Annot t -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (Annot t)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Annot t)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Annot t -> Doc

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

type Rep (Annot t)

Defined in Language.Haskell.Liquid.Types.Types

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

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

Constructors

HoleInfo

Fields

• htype :: t
• hloc :: SrcSpan
• henv :: AREnv t
• info :: i

Instances

Functor (HoleInfo i)

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)

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

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

Constructors

O

Fields

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

Instances

Functor Output

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

FromJSON (Output Doc)

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

parseJSON :: Value -> Parser (Output Doc)

parseJSONList :: Value -> Parser [Output Doc]

omittedField :: Maybe (Output Doc)

ToJSON (Output Doc)

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

toJSON :: Output Doc -> Value

toEncoding :: Output Doc -> Encoding

toJSONList :: [Output Doc] -> Value

toEncodingList :: [Output Doc] -> Encoding

omitField :: Output Doc -> Bool

Monoid (Output a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: Output a

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

mconcat :: [Output a] -> Output a

Semigroup (Output a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

Generic (Output a)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (Output a)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Output a -> Doc

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

type Rep (Output a)

Defined in Language.Haskell.Liquid.Types.Types

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

isHole :: Expr -> Bool

hasHole :: Reftable r => r -> Bool

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

PPrint Class

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Class -> Doc

pprintPrec :: Int -> Tidy -> Class -> Doc

PPrint DataCon

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataCon -> Doc

pprintPrec :: Int -> Tidy -> DataCon -> Doc

PPrint Type

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Type -> Doc

pprintPrec :: Int -> Tidy -> Type -> Doc

PPrint TyCon

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> TyCon -> Doc

pprintPrec :: Int -> Tidy -> TyCon -> Doc

PPrint Name

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Name -> Doc

pprintPrec :: Int -> Tidy -> Name -> Doc

PPrint SourceError

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

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> SourceError -> Doc

pprintPrec :: Int -> Tidy -> SourceError -> Doc

PPrint SrcSpan

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc

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

PPrint TyThing

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> TyThing -> Doc

pprintPrec :: Int -> Tidy -> TyThing -> Doc

PPrint Var

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Var -> Doc

pprintPrec :: Int -> Tidy -> Var -> Doc

PPrint CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> CVertex -> Doc

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

PPrint KVGraph

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> KVGraph -> Doc

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

PPrint Rank

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> Rank -> Doc

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

PPrint Pred

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Pred -> Doc

pprintPrec :: Int -> Tidy -> Pred -> Doc

PPrint Tag

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Tag -> Doc

pprintPrec :: Int -> Tidy -> Tag -> Doc

PPrint Command

Defined in Language.Fixpoint.Smt.Types

Methods

pprintTidy :: Tidy -> Command -> Doc

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

PPrint Recur

Defined in Language.Fixpoint.Solver.Instantiate

Methods

pprintTidy :: Tidy -> Recur -> Doc

pprintPrec :: Int -> Tidy -> Recur -> Doc

PPrint TermOrigin

Defined in Language.Fixpoint.Solver.Rewrite

Methods

pprintTidy :: Tidy -> TermOrigin -> Doc

pprintPrec :: Int -> Tidy -> TermOrigin -> Doc

PPrint WorkItem

Defined in Language.Fixpoint.Solver.Worklist

Methods

pprintTidy :: Tidy -> WorkItem -> Doc

pprintPrec :: Int -> Tidy -> WorkItem -> Doc

PPrint AxiomEnv

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> AxiomEnv -> Doc

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

PPrint Equation

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> Equation -> Doc

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

PPrint GFixSolution

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> GFixSolution -> Doc

pprintPrec :: Int -> Tidy -> GFixSolution -> Doc

PPrint QualParam

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> QualParam -> Doc

pprintPrec :: Int -> Tidy -> QualParam -> Doc

PPrint QualPattern

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> QualPattern -> Doc

pprintPrec :: Int -> Tidy -> QualPattern -> Doc

PPrint Rewrite

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> Rewrite -> Doc

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

PPrint IBindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> IBindEnv -> Doc

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

PPrint Packs

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> Packs -> Doc

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

PPrint Error

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error -> Doc

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

PPrint Error1

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error1 -> Doc

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

PPrint Symbol

Defined in Language.Fixpoint.Types.Names

Methods

pprintTidy :: Tidy -> Symbol -> Doc

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

PPrint DocTable

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> DocTable -> Doc

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

PPrint Tidy

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Tidy -> Doc

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

PPrint Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Bop -> Doc

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

PPrint Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Brel -> Doc

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

PPrint Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Constant -> Doc

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

PPrint KVSub

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVSub -> Doc

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

PPrint KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVar -> Doc

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

PPrint SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SymConst -> Doc

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

PPrint BIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BIndex -> Doc

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

PPrint BindPred

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BindPred -> Doc

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

PPrint Cube

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> Cube -> Doc

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

PPrint EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EQual -> Doc

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

PPrint EbindSol

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EbindSol -> Doc

pprintPrec :: Int -> Tidy -> EbindSol -> Doc

PPrint KIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> KIndex -> Doc

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

PPrint QBind

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> QBind -> Doc

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

PPrint DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataCtor -> Doc

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

PPrint DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataDecl -> Doc

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

PPrint DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataField -> Doc

pprintPrec :: Int -> Tidy -> DataField -> Doc

PPrint FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> FTycon -> Doc

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

PPrint Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> Sort -> Doc

pprintPrec :: Int -> Tidy -> Sort -> Doc

PPrint TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCArgs -> Doc

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

PPrint SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc

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

PPrint Templates

Defined in Language.Fixpoint.Types.Templates

Methods

pprintTidy :: Tidy -> Templates -> Doc

pprintPrec :: Int -> Tidy -> Templates -> Doc

PPrint Sem

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> Sem -> Doc

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

PPrint SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> SmtSort -> Doc

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

PPrint TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> TheorySymbol -> Doc

pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc

PPrint Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Trigger -> Doc

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

PPrint Stats

Defined in Language.Fixpoint.Utils.Statistics

Methods

pprintTidy :: Tidy -> Stats -> Doc

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

PPrint CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGEnv -> Doc

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

PPrint CGInfo

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> CGInfo -> Doc

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

PPrint SubC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> SubC -> Doc

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

PPrint WfC

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

pprintTidy :: Tidy -> WfC -> Doc

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

PPrint Pattern

Defined in Language.Haskell.Liquid.GHC.Resugar

Methods

pprintTidy :: Tidy -> Pattern -> Doc

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

PPrint BPspec

Defined in Language.Haskell.Liquid.Parse

Methods

pprintTidy :: Tidy -> BPspec -> Doc

pprintPrec :: Int -> Tidy -> BPspec -> Doc

PPrint SpecType => PPrint DataConP

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataConP -> Doc

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

PPrint DataName

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataName -> Doc

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

PPrint HasDataDecl

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> HasDataDecl -> Doc

pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc

PPrint Oblig

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc

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

PPrint ParseError

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> ParseError -> Doc

pprintPrec :: Int -> Tidy -> ParseError -> Doc

PPrint UserError

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> UserError -> Doc

pprintPrec :: Int -> Tidy -> UserError -> Doc

PPrint LHName

Defined in Language.Haskell.Liquid.Types.Names

Methods

pprintTidy :: Tidy -> LHName -> Doc

pprintPrec :: Int -> Tidy -> LHName -> Doc

PPrint BTyCon

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> BTyCon -> Doc

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

PPrint BTyVar

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> BTyVar -> Doc

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

PPrint Predicate

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> Predicate -> Doc

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

PPrint RTyCon

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> RTyCon -> Doc

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

PPrint RTyVar

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> RTyVar -> Doc

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

PPrint TyConP

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> TyConP -> Doc

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

PPrint TargetInfo

Defined in Language.Haskell.Liquid.GHC.Interface

Methods

pprintTidy :: Tidy -> TargetInfo -> Doc

pprintPrec :: Int -> Tidy -> TargetInfo -> Doc

PPrint TargetSpec

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

Defined in Language.Haskell.Liquid.GHC.Interface

Methods

pprintTidy :: Tidy -> TargetSpec -> Doc

pprintPrec :: Int -> Tidy -> TargetSpec -> Doc

PPrint Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Cinfo -> Doc

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

PPrint Error

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc

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

PPrint KVKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVKind -> Doc

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

PPrint KVProf

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVProf -> Doc

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

PPrint LogicMap

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LogicMap -> Doc

pprintPrec :: Int -> Tidy -> LogicMap -> Doc

PPrint ModName

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> ModName -> Doc

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

PPrint RelExpr

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RelExpr -> Doc

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

PPrint Variance

Defined in Language.Haskell.Liquid.Types.Variance

Methods

pprintTidy :: Tidy -> Variance -> Doc

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

PPrint Def

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

pprintTidy :: Tidy -> Def -> Doc

pprintPrec :: Int -> Tidy -> Def -> Doc

PPrint DiffCheck

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

pprintTidy :: Tidy -> DiffCheck -> Doc

pprintPrec :: Int -> Tidy -> DiffCheck -> Doc

PPrint Doc

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Doc -> Doc

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

PPrint Text

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Text -> Doc

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

PPrint Integer

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Integer -> Doc

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

PPrint ()

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> () -> Doc

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

PPrint Bool

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bool -> Doc

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

PPrint Char

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Char -> Doc

pprintPrec :: Int -> Tidy -> Char -> Doc

PPrint Float

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Float -> Doc

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

PPrint Int

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Int -> Doc

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

PPrint (Bind Var)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Bind Var -> Doc

pprintPrec :: Int -> Tidy -> Bind Var -> Doc

PPrint (Expr Var)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Expr Var -> Doc

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

PPrint (Elims a)

Defined in Language.Fixpoint.Graph.Deps

Methods

pprintTidy :: Tidy -> Elims a -> Doc

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

PPrint (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Bind a -> Doc

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

PPrint (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Cstr a -> Doc

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

PPrint (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Query a -> Doc

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

PPrint (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Var a -> Doc

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

PPrint (Worklist a)

Defined in Language.Fixpoint.Solver.Worklist

Methods

pprintTidy :: Tidy -> Worklist a -> Doc

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

PPrint (QualifierV v)

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> QualifierV v -> Doc

pprintPrec :: Int -> Tidy -> QualifierV v -> Doc

Fixpoint a => PPrint (SimpC a)

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> SimpC a -> Doc

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

Fixpoint a => PPrint (SubC a)

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> SubC a -> Doc

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

Fixpoint a => PPrint (WfC a)

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> WfC a -> Doc

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

PPrint a => PPrint (SEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> SEnv a -> Doc

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

PPrint a => PPrint (SizedEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

pprintTidy :: Tidy -> SizedEnv a -> Doc

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

Fixpoint a => PPrint (FixResult a)

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)

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)

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SubstV v -> Doc

pprintPrec :: Int -> Tidy -> SubstV v -> Doc

PPrint a => PPrint (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCEmb a -> Doc

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

PPrint a => PPrint (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> Located a -> Doc

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

PPrint a => PPrint (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Triggered a -> Doc

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

Show a => PPrint (Trie a)

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)

Defined in Language.Haskell.Liquid.Bare.Types

Methods

pprintTidy :: Tidy -> PlugTV v -> Doc

pprintPrec :: Int -> Tidy -> PlugTV v -> Doc

PPrint a => PPrint (Template a)

Defined in Language.Haskell.Liquid.Constraint.Template

Methods

pprintTidy :: Tidy -> Template a -> Doc

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

PPrint ty => PPrint (DataCtorP ty)

Defined in Language.Haskell.Liquid.Types.DataDecl

Methods

pprintTidy :: Tidy -> DataCtorP ty -> Doc

pprintPrec :: Int -> Tidy -> DataCtorP ty -> Doc

PPrint (CtxError SpecType)

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> CtxError SpecType -> Doc

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

PPrint (CtxError Doc)

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.

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> CtxError Doc -> Doc

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

PPrint (PVar a)

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> PVar a -> Doc

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

PPrint v => PPrint (SizeFunV v)

Defined in Language.Haskell.Liquid.Types.RType

Methods

pprintTidy :: Tidy -> SizeFunV v -> Doc

pprintPrec :: Int -> Tidy -> SizeFunV v -> Doc

PPrint t => PPrint (AREnv t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> AREnv t -> Doc

pprintPrec :: Int -> Tidy -> AREnv t -> Doc

PPrint a => PPrint (AnnInfo a)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> AnnInfo a -> Doc

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

PPrint t => PPrint (Annot t)

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BodyV v -> Doc

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

PPrint t => PPrint (CMeasure t)

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)

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LMapV v -> Doc

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

PPrint a => PPrint (Output a)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Output a -> Doc

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

PPrint t => PPrint (RClass t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RClass t -> Doc

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

PPrint t => PPrint (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RISig t -> Doc

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

PPrint t => PPrint (RInstance t)

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)

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> HashSet a -> Doc

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

PPrint a => PPrint (Maybe a)

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> Maybe a -> Doc

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

PPrint a => PPrint [a]

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

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

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)

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)

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)

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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

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)

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)

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)

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)

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)

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

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

Constructors

ModName !ModType !ModuleName

Instances

Data ModName

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: ModName -> Constr

dataTypeOf :: ModName -> DataType

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

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

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

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

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

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

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

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

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

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

Generic ModName

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep ModName

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> ModName -> ShowS

show :: ModName -> String

showList :: [ModName] -> ShowS

Eq ModName

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Ord ModName

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> ModName -> Int

hash :: ModName -> Int

Symbolic ModName

Defined in Language.Haskell.Liquid.Types.Types

Methods

symbol :: ModName -> Symbol

PPrint ModName

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> ModName -> Doc

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

type Rep ModName

Defined in Language.Haskell.Liquid.Types.Types

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

Constructors

Target

SrcImport

SpecImport

Instances

Data ModType

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: ModType -> Constr

dataTypeOf :: ModType -> DataType

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

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

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

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

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

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

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

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

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

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

Generic ModType

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep ModType

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> ModType -> ShowS

show :: ModType -> String

showList :: [ModType] -> ShowS

Eq ModType

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Ord ModType

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> ModType -> Int

hash :: ModType -> Int

type Rep ModType

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

isSrcImport :: ModName -> Bool

isSpecImport :: ModName -> Bool

isTarget :: ModName -> Bool

getModName :: ModName -> ModuleName

getModString :: ModName -> String

Refinement Type Aliases

data RTEnv tv t

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

Constructors

RTE

Fields

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

Instances

Monoid (RTEnv tv t)

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)

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)

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

type SpecRTEnv = RTEnv RTyVar SpecType

type BareRTAlias = RTAlias Symbol BareType

type SpecRTAlias = RTAlias RTyVar SpecType

Diagnostics, Warnings, Errors and Error Messages

type Error = TError SpecType

type ErrorResult = FixResult UserError

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

data Warning

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

Instances

Show Warning

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

Eq Warning

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

mkWarning :: SrcSpan -> Doc -> Warning

data Diagnostics

Instances

Monoid Diagnostics

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: Diagnostics

mappend :: Diagnostics -> Diagnostics -> Diagnostics

mconcat :: [Diagnostics] -> Diagnostics

Semigroup Diagnostics

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: Diagnostics -> Diagnostics -> Diagnostics

sconcat :: NonEmpty Diagnostics -> Diagnostics

stimes :: Integral b => b -> Diagnostics -> Diagnostics

Eq Diagnostics

Defined in Language.Haskell.Liquid.Types.Types

Methods

(==) :: Diagnostics -> Diagnostics -> Bool

(/=) :: Diagnostics -> Diagnostics -> Bool

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

emptyDiagnostics :: Diagnostics

noErrors :: Diagnostics -> Bool

allWarnings :: Diagnostics -> [Warning]

allErrors :: Diagnostics -> [Error]

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

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

Source information (associated with constraints)

data Cinfo

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

Constructors

Ci

Fields

• ci_loc :: !SrcSpan
• ci_err :: !(Maybe Error)
• ci_var :: !(Maybe Var)

Instances

NFData Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: Cinfo -> ()

Generic Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep Cinfo

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Cinfo -> ShowS

show :: Cinfo -> String

showList :: [Cinfo] -> ShowS

Eq Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Fixpoint Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

toFix :: Cinfo -> Doc

simplify :: Cinfo -> Cinfo

PPrint Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> Cinfo -> Doc

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

Loc Cinfo

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: Cinfo -> SrcSpan

Result (FixResult Cinfo)

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

result :: FixResult Cinfo -> FixResult UserError

type Rep Cinfo

Defined in Language.Haskell.Liquid.Types.Types

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

data MeasureV v ty ctor

Constructors

M

Fields

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

Instances

Expand BareMeasure

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure

Bifunctor (MeasureV v)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Measure ty ctor -> [Symbol]

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

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

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

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

Loc (Measure a b)

Defined in Language.Haskell.Liquid.Types.Types

Methods

srcSpan :: Measure a b -> SrcSpan

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

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (MeasureV v ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

type Rep (MeasureV v ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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]

type UnSortedExpr = ([Symbol], Expr)

data MeasureKind

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

Binary MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: MeasureKind -> Put

get :: Get MeasureKind

putList :: [MeasureKind] -> Put

Data MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: MeasureKind -> Constr

dataTypeOf :: MeasureKind -> DataType

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

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

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

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

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

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

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

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

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

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

Generic MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> MeasureKind -> ShowS

show :: MeasureKind -> String

showList :: [MeasureKind] -> ShowS

Eq MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Ord MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> MeasureKind -> Int

hash :: MeasureKind -> Int

type Rep MeasureKind

Defined in Language.Haskell.Liquid.Types.Types

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

Constructors

CM

Fields

• cName :: Located LHName
• cSort :: ty

Instances

Functor CMeasure

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Data ty => Data (CMeasure ty)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: CMeasure ty -> Constr

dataTypeOf :: CMeasure ty -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (CMeasure ty)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (CMeasure ty)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> CMeasure t -> ShowS

show :: CMeasure t -> String

showList :: [CMeasure t] -> ShowS

PPrint t => PPrint (CMeasure t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> CMeasure t -> Doc

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

type Rep (CMeasure ty)

Defined in Language.Haskell.Liquid.Types.Types

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

data DefV v ty ctor

Constructors

Def

Fields

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

Instances

Expand BareDef

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef

Bifunctor (DefV v)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Def ty ctor -> [Symbol]

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

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

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

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

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

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (DefV v ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

type Rep (DefV v ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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

Measures

data BodyV v

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

Functor BodyV

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable BodyV

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: Body -> [Symbol]

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

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

subst :: Subst -> Body -> Body

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

Expand Body

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> Body -> Body

Binary v => Binary (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: BodyV v -> Put

get :: Get (BodyV v)

putList :: [BodyV v] -> Put

Data v => Data (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> BodyV v -> ShowS

show :: BodyV v -> String

showList :: [BodyV v] -> ShowS

Eq v => Eq (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Hashable v => Hashable (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> BodyV v -> Int

hash :: BodyV v -> Int

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> BodyV v -> Doc

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

type Rep (BodyV v)

Defined in Language.Haskell.Liquid.Types.Types

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

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

Bifunctor MSpec

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

Functor (MSpec ty)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Eq ctor => Monoid (MSpec ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: MSpec ty ctor

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

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

Eq ctor => Semigroup (MSpec ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: MSpec ty ctor -> Constr

dataTypeOf :: MSpec ty ctor -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (MSpec ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (MSpec ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

show :: MSpec ty ctor -> String

showList :: [MSpec ty ctor] -> ShowS

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

type Rep (MSpec ty ctor)

Defined in Language.Haskell.Liquid.Types.Types

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

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

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

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

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

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

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

Type Classes

data RClass ty

Constructors

RClass

Fields

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

Instances

Functor RClass

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable RClass

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RClass ty -> Put

get :: Get (RClass ty)

putList :: [RClass ty] -> Put

Data ty => Data (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: RClass ty -> Constr

dataTypeOf :: RClass ty -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RClass ty -> ShowS

show :: RClass ty -> String

showList :: [RClass ty] -> ShowS

Eq ty => Eq (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Hashable ty => Hashable (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RClass ty -> Int

hash :: RClass ty -> Int

PPrint t => PPrint (RClass t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RClass t -> Doc

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

type Rep (RClass ty)

Defined in Language.Haskell.Liquid.Types.Types

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

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

NFData KVKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: KVKind -> ()

Data KVKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: KVKind -> Constr

dataTypeOf :: KVKind -> DataType

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

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

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

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

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

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

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

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

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

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

Generic KVKind

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep KVKind

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> KVKind -> ShowS

show :: KVKind -> String

showList :: [KVKind] -> ShowS

Eq KVKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Ord KVKind

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> KVKind -> Int

hash :: KVKind -> Int

PPrint KVKind

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVKind -> Doc

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

type Rep KVKind

Defined in Language.Haskell.Liquid.Types.Types

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

Instances

NFData KVProf

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: KVProf -> ()

Generic KVProf

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep KVProf

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> KVProf -> Doc

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

type Rep KVProf

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

emptyKVProf :: KVProf

updKVProf :: KVKind -> Kuts -> KVProf -> KVProf

Misc

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

CoreToLogic

data LogicMap

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

Monoid LogicMap

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: LogicMap

mappend :: LogicMap -> LogicMap -> LogicMap

mconcat :: [LogicMap] -> LogicMap

Semigroup LogicMap

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: LogicMap -> LogicMap -> LogicMap

sconcat :: NonEmpty LogicMap -> LogicMap

stimes :: Integral b => b -> LogicMap -> LogicMap

Show LogicMap

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> LogicMap -> ShowS

show :: LogicMap -> String

showList :: [LogicMap] -> ShowS

PPrint LogicMap

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)

mkLogicMap :: HashMap Symbol LMap -> LogicMap

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

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

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

data LMapV v

Constructors

LMap

Fields

• lmVar :: LocSymbol
• lmArgs :: [Symbol]
• lmExpr :: ExprV v

Instances

Functor LMapV

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Binary v => Binary (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: LMapV v -> Put

get :: Get (LMapV v)

putList :: [LMapV v] -> Put

Data v => Data (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> LMapV v -> ShowS

show :: LMapV v -> String

showList :: [LMapV v] -> ShowS

Eq v => Eq (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Hashable v => Hashable (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> LMapV v -> Int

hash :: LMapV v -> Int

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

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

pprintTidy :: Tidy -> LMapV v -> Doc

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

type Rep (LMapV v)

Defined in Language.Haskell.Liquid.Types.Types

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

Refined Instances

type RDEnv = DEnv Var SpecType

newtype DEnv x ty

Constructors

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

Instances

Functor (DEnv x)

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)

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)

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)

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

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

Functor RInstance

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable RInstance

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RInstance t -> Put

get :: Get (RInstance t)

putList :: [RInstance t] -> Put

Data t => Data (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: RInstance t -> Constr

dataTypeOf :: RInstance t -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RInstance t -> ShowS

show :: RInstance t -> String

showList :: [RInstance t] -> ShowS

Eq t => Eq (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Hashable t => Hashable (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RInstance t -> Int

hash :: RInstance t -> Int

PPrint t => PPrint (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RInstance t -> Doc

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

type Rep (RInstance t)

Defined in Language.Haskell.Liquid.Types.Types

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

Constructors

RIAssumed t

RISig t

Instances

Functor RISig

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Foldable RISig

Defined in Language.Haskell.Liquid.Types.Types

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

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

put :: RISig t -> Put

get :: Get (RISig t)

putList :: [RISig t] -> Put

Data t => Data (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

toConstr :: RISig t -> Constr

dataTypeOf :: RISig t -> DataType

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

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

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

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

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

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

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

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

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

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

Generic (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

type Rep (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

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)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> RISig t -> ShowS

show :: RISig t -> String

showList :: [RISig t] -> ShowS

Eq t => Eq (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

Hashable t => Hashable (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

hashWithSalt :: Int -> RISig t -> Int

hash :: RISig t -> Int

PPrint t => PPrint (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

pprintTidy :: Tidy -> RISig t -> Doc

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

type Rep (RISig t)

Defined in Language.Haskell.Liquid.Types.Types

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

data MethodType t

Constructors

MT

Fields

• tyInstance :: !(Maybe t)
• tyClass :: !(Maybe t)

Instances

Show t => Show (MethodType t)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> MethodType t -> ShowS

show :: MethodType t -> String

showList :: [MethodType t] -> ShowS

getMethodType :: MethodType t -> Maybe t

String Literals

liquidBegin :: String

liquidEnd :: String

data Axiom b s e

Values Related to Specifications ------------------------------------

Constructors

Axiom

Fields

• aname :: (Var, Maybe DataCon)
• rname :: Maybe b
• abinds :: [b]
• atypes :: [s]
• alhs :: e
• arhs :: e

Instances

Show (Axiom Var Type CoreExpr)

Defined in Language.Haskell.Liquid.Types.Types

Methods

showsPrec :: Int -> Axiom Var Type CoreExpr -> ShowS

show :: Axiom Var Type CoreExpr -> String

showList :: [Axiom Var Type CoreExpr] -> ShowS

type HAxiom = Axiom Var Type CoreExpr

ordSrcSpan :: SrcSpan -> SrcSpan -> Ordering

Orphan instances

Ord DataCon

Methods

compare :: DataCon -> DataCon -> Ordering

(<) :: DataCon -> DataCon -> Bool

(<=) :: DataCon -> DataCon -> Bool

(>) :: DataCon -> DataCon -> Bool

(>=) :: DataCon -> DataCon -> Bool

max :: DataCon -> DataCon -> DataCon

min :: DataCon -> DataCon -> DataCon

Ord TyCon

Methods

compare :: TyCon -> TyCon -> Ordering

(<) :: TyCon -> TyCon -> Bool

(<=) :: TyCon -> TyCon -> Bool

(>) :: TyCon -> TyCon -> Bool

(>=) :: TyCon -> TyCon -> Bool

max :: TyCon -> TyCon -> TyCon

min :: TyCon -> TyCon -> TyCon

Symbolic DataCon

Methods

symbol :: DataCon -> Symbol

Symbolic ModuleName

Methods

symbol :: ModuleName -> Symbol

PPrint TyThing

Methods

pprintTidy :: Tidy -> TyThing -> Doc

pprintPrec :: Int -> Tidy -> TyThing -> Doc

NFData a => NFData (TError a)

Methods

rnf :: TError a -> ()

Subable t => Subable (WithModel t)

Methods

syms :: WithModel t -> [Symbol]

substa :: (Symbol -> Symbol) -> WithModel t -> WithModel t

substf :: (Symbol -> Expr) -> WithModel t -> WithModel t

subst :: Subst -> WithModel t -> WithModel t

subst1 :: WithModel t -> (Symbol, Expr) -> WithModel t