Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Types

Contents

Options
Ghc Information
F.Located Things
Symbols
Default unknown name
Bare Type Constructors and Variables
Refined Type Constructors
Refinement Types
Worlds
Classes describing operations on RTypes
Type Variables
Predicate Variables
Refinements
Parse-time entities describing refined data types
Pre-instantiated RType
Instantiated RType
Constructing & Destructing RTypes
Manipulating Predicates
Some tests on RTypes
Traversing RType
???
Inferred Annotations
Hole Information
Overall Output
Refinement Hole
Converting To and From Sort
Class for values that can be pretty printed
Printer Configuration
Modules and Imports
Refinement Type Aliases
Diagnostics, Warnings, Errors and Error Messages
Source information (associated with constraints)
Measures
Scoping Info
Type Classes
KV Profiling
Misc
CoreToLogic
Refined Instances
Ureftable Instances
String Literals
Orphan instances

Description

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

Synopsis

module Language.Haskell.Liquid.UX.Config
data TargetVars
- = AllVars
- | Only ![Var]
data TyConMap = TyConMap {
- tcmTyRTy :: HashMap TyCon RTyCon
- tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon
- tcmFtcArity :: HashMap TyCon Int
}
data Located a = Loc {
- loc :: !SourcePos
- locE :: !SourcePos
- val :: !a
}
dummyLoc :: a -> Located a
type LocSymbol = Located Symbol
type LocText = Located Text
dummyName :: Symbol
isDummy :: Symbolic a => a -> Bool
data BTyCon = BTyCon {
- btc_tc :: !LocSymbol
- btc_class :: !Bool
- btc_prom :: !Bool
}
mkBTyCon :: LocSymbol -> BTyCon
isClassBTyCon :: BTyCon -> Bool
newtype BTyVar = BTV Symbol
data RTyCon = RTyCon TyCon ![RPVar] !TyConInfo
data TyConInfo = TyConInfo {
- varianceTyArgs :: !VarianceInfo
- variancePsArgs :: !VarianceInfo
- sizeFunction :: !(Maybe SizeFun)
}
defaultTyConInfo :: TyConInfo
rTyConPVs :: RTyCon -> [RPVar]
rTyConPropVs :: RTyCon -> [PVar RSort]
isClassType :: TyConable c => RType c t t1 -> Bool
isEqType :: TyConable c => RType c t t1 -> Bool
isRVar :: RType c tv r -> Bool
isBool :: RType RTyCon t t1 -> Bool
data RType c tv r
- = RVar {
  - rt_var :: !tv
  - rt_reft :: !r
  }
- | RFun {
  - rt_bind :: !Symbol
  - rt_in :: !(RType c tv r)
  - rt_out :: !(RType c tv r)
  - rt_reft :: !r
  }
- | RImpF {
  - rt_bind :: !Symbol
  - rt_in :: !(RType c tv r)
  - rt_out :: !(RType c tv r)
  - rt_reft :: !r
  }
- | RAllT {
  - rt_tvbind :: !(RTVU c tv)
  - rt_ty :: !(RType c tv r)
  - rt_ref :: !r
  }
- | RAllP {
  - rt_pvbind :: !(PVU c tv)
  - rt_ty :: !(RType c tv r)
  }
- | RApp {
  - rt_tycon :: !c
  - rt_args :: ![RType c tv r]
  - rt_pargs :: ![RTProp c tv r]
  - rt_reft :: !r
  }
- | RAllE {
  - rt_bind :: !Symbol
  - rt_allarg :: !(RType c tv r)
  - rt_ty :: !(RType c tv r)
  }
- | REx {
  - rt_bind :: !Symbol
  - rt_exarg :: !(RType c tv r)
  - rt_ty :: !(RType c tv r)
  }
- | RExprArg (Located Expr)
- | RAppTy {
  - rt_arg :: !(RType c tv r)
  - rt_res :: !(RType c tv r)
  - rt_reft :: !r
  }
- | RRTy {
  - rt_env :: ![(Symbol, RType c tv r)]
  - rt_ref :: !r
  - rt_obl :: !Oblig
  - rt_ty :: !(RType c tv r)
  }
- | RHole r
data Ref τ t = RProp {
- rf_args :: [(Symbol, τ)]
- rf_body :: t
}
type RTProp c tv r = Ref (RType c tv ()) (RType c tv r)
rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
newtype RTyVar = RTV TyVar
data RTAlias x a = RTA {
- rtName :: Symbol
- rtTArgs :: [x]
- rtVArgs :: [Symbol]
- rtBody :: a
}
type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv)
lmapEAlias :: LMap -> Located (RTAlias Symbol Expr)
dropImplicits :: RType c tv r -> RType c tv r
data HSeg t
- = HBind {
  - hs_addr :: !Symbol
  - hs_val :: t
  }
- | HVar UsedPVar
newtype World t = World [HSeg t]
class Eq c => TyConable c where
- isFun :: c -> Bool
- isList :: c -> Bool
- isTuple :: c -> Bool
- ppTycon :: c -> Doc
- isClass :: c -> Bool
- isEqual :: c -> Bool
- isNumCls :: c -> Bool
- isFracCls :: c -> Bool
class SubsTy tv ty a where
- subt :: (tv, ty) -> a -> a
data RTVar tv s = RTVar {
- ty_var_value :: tv
- ty_var_info :: RTVInfo s
}
data RTVInfo s
- = RTVNoInfo {
  - rtv_is_pol :: Bool
  }
- | RTVInfo {
  - rtv_name :: Symbol
  - rtv_kind :: s
  - rtv_is_val :: Bool
  - rtv_is_pol :: Bool
  }
makeRTVar :: tv -> RTVar tv s
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2
rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s)
setRtvPol :: RTVar tv a -> Bool -> RTVar tv a
data PVar t = PV {
- pname :: !Symbol
- ptype :: !(PVKind t)
- parg :: !Symbol
- pargs :: ![(t, Symbol, Expr)]
}
isPropPV :: PVar t -> Bool
pvType :: PVar t -> t
data PVKind t
- = PVProp t
- | PVHProp
newtype Predicate = Pr [UsedPVar]
data UReft r = MkUReft {
- ur_reft :: !r
- ur_pred :: !Predicate
}
data SizeFun
- = IdSizeFun
- | SymSizeFun LocSymbol
szFun :: SizeFun -> Symbol -> Expr
data DataDecl = DataDecl {
- tycName :: DataName
- tycTyVars :: [Symbol]
- tycPVars :: [PVar BSort]
- tycDCons :: [DataCtor]
- tycSrcPos :: !SourcePos
- tycSFun :: Maybe SizeFun
- tycPropTy :: Maybe BareType
- tycKind :: !DataDeclKind
}
data DataName
- = DnName !LocSymbol
- | DnCon !LocSymbol
dataNameSymbol :: DataName -> LocSymbol
data DataCtor = DataCtor {
- dcName :: LocSymbol
- dcTyVars :: [Symbol]
- dcTheta :: [BareType]
- dcFields :: [(Symbol, BareType)]
- dcResult :: Maybe BareType
}
data DataConP = DataConP {
- dcpLoc :: !SourcePos
- dcpCon :: !DataCon
- dcpFreeTyVars :: ![RTyVar]
- dcpFreePred :: ![PVar RSort]
- dcpTyConstrs :: ![SpecType]
- dcpTyArgs :: ![(Symbol, SpecType)]
- dcpTyRes :: !SpecType
- dcpIsGadt :: !Bool
- dcpModule :: !Symbol
- dcpLocE :: !SourcePos
}
data HasDataDecl
- = NoDecl (Maybe SizeFun)
- | HasDecl
hasDecl :: DataDecl -> HasDataDecl
data DataDeclKind
- = DataUser
- | DataReflected
data TyConP = TyConP {
- tcpLoc :: !SourcePos
- tcpCon :: !TyCon
- tcpFreeTyVarsTy :: ![RTyVar]
- tcpFreePredTy :: ![PVar RSort]
- tcpVarianceTs :: !VarianceInfo
- tcpVariancePs :: !VarianceInfo
- tcpSizeFun :: !(Maybe SizeFun)
}
type RRType = RType RTyCon RTyVar
type RRProp r = Ref RSort (RRType r)
type BRType = RType BTyCon BTyVar
type BRProp r = Ref BSort (BRType r)
type BSort = BRType ()
type BPVar = PVar BSort
type RTVU c tv = RTVar tv (RType c tv ())
type PVU c tv = PVar (RType c tv ())
type BareType = BRType RReft
type PrType = RRType Predicate
type SpecType = RRType RReft
type SpecProp = RRProp RReft
type SpecRTVar = RTVar RTyVar RSort
type SpecRep = RRep RReft
type LocBareType = Located BareType
type LocSpecType = Located SpecType
type RSort = RRType ()
type UsedPVar = PVar ()
type RPVar = PVar RSort
type RReft = UReft Reft
type REnv = AREnv SpecType
data AREnv t = REnv {
- reGlobal :: HashMap Symbol t
- reLocal :: HashMap Symbol t
}
data RTypeRep c tv r = RTypeRep {
- ty_vars :: [(RTVar tv (RType c tv ()), r)]
- ty_preds :: [PVar (RType c tv ())]
- ty_ebinds :: [Symbol]
- ty_erefts :: [r]
- ty_eargs :: [RType c tv r]
- ty_binds :: [Symbol]
- ty_refts :: [r]
- ty_args :: [RType c tv r]
- ty_res :: RType c tv r
}
fromRTypeRep :: RTypeRep c tv r -> RType c tv r
toRTypeRep :: RType c tv r -> RTypeRep c tv r
mkArrow :: [(RTVar tv (RType c tv ()), r)] -> [PVar (RType c tv ())] -> [(Symbol, RType c tv r, r)] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv r
bkArrowDeep :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkArrow :: RType t t1 a -> (([Symbol], [RType t t1 a], [a]), ([Symbol], [RType t t1 a], [a]), RType t t1 a)
safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RType t t1 a], [a]), ([Symbol], [RType t t1 a], [a]), RType t t1 a)
mkUnivs :: (Foldable t, Foldable t1) => t (RTVar tv (RType c tv ()), r) -> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
bkUniv :: RType tv c r -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())], RType tv c r)
bkClass :: (PPrint c, TyConable c) => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])], SpecType)
rImpF :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r
pvars :: Predicate -> [UsedPVar]
pappSym :: Show a => a -> Symbol
pApp :: Symbol -> [Expr] -> Expr
isBase :: RType t t1 t2 -> Bool
isFunTy :: RType t t1 t2 -> Bool
isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool
hasHole :: Reftable r => r -> Bool
efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b
foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType c tv r1 -> RType c tv r2
mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r)
mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
data Oblig
- = OTerm
- | OInv
- | OCons
ignoreOblig :: RType t t1 t2 -> RType t t1 t2
addInvCond :: SpecType -> RReft -> SpecType
newtype AnnInfo a = AI (HashMap SrcSpan [(Maybe Text, a)])
data Annot t
- = AnnUse t
- | AnnDef t
- | AnnRDf t
- | AnnLoc SrcSpan
data HoleInfo i t = HoleInfo {
- htype :: t
- hloc :: SrcSpan
- henv :: AREnv t
- info :: i
}
data Output a = O {
- o_vars :: Maybe [String]
- o_types :: !(AnnInfo a)
- o_templs :: !(AnnInfo a)
- o_bots :: ![SrcSpan]
- o_result :: ErrorResult
}
hole :: Expr
isHole :: Expr -> Bool
hasHoleTy :: RType t t1 t2 -> Bool
ofRSort :: Reftable r => RType c tv () -> RType c tv r
toRSort :: RType c tv r -> RType c tv ()
rTypeValueVar :: Reftable r => RType c tv r -> Symbol
rTypeReft :: Reftable r => RType c tv r -> Reft
stripRTypeBase :: RType c tv r -> Maybe r
topRTypeBase :: Reftable r => RType c tv r -> RType c tv r
class PPrint a where
- pprintTidy :: Tidy -> a -> Doc
- pprintPrec :: Int -> Tidy -> a -> Doc
pprint :: PPrint a => a -> Doc
showpp :: PPrint a => a -> String
data PPEnv = PP {
- ppPs :: Bool
- ppTyVar :: Bool
- ppShort :: Bool
- ppDebug :: Bool
}
ppEnv :: PPEnv
ppEnvShort :: PPEnv -> PPEnv
data ModName = ModName !ModType !ModuleName
data ModType
- = Target
- | SrcImport
- | SpecImport
isSrcImport :: ModName -> Bool
isSpecImport :: ModName -> Bool
isTarget :: ModName -> Bool
getModName :: ModName -> ModuleName
getModString :: ModName -> String
qualifyModName :: ModName -> Symbol -> Symbol
data RTEnv tv t = RTE {
- typeAliases :: HashMap Symbol (Located (RTAlias tv t))
- exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))
}
type BareRTEnv = RTEnv Symbol BareType
type SpecRTEnv = RTEnv RTyVar SpecType
type BareRTAlias = RTAlias Symbol BareType
type SpecRTAlias = RTAlias RTyVar SpecType
module Language.Haskell.Liquid.Types.Errors
type Error = TError SpecType
type ErrorResult = FixResult UserError
data Warning
mkWarning :: SrcSpan -> Doc -> Warning
data Diagnostics
mkDiagnostics :: [Warning] -> [Error] -> Diagnostics
emptyDiagnostics :: Diagnostics
noErrors :: Diagnostics -> Bool
allWarnings :: Diagnostics -> [Warning]
allErrors :: Diagnostics -> [Error]
printWarning :: DynFlags -> Warning -> IO ()
data Cinfo = Ci {
- ci_loc :: !SrcSpan
- ci_err :: !(Maybe Error)
- ci_var :: !(Maybe Var)
}
data Measure ty ctor = M {
- msName :: LocSymbol
- msSort :: ty
- msEqns :: [Def ty ctor]
- msKind :: !MeasureKind
- msUnSorted :: !UnSortedExprs
}
type UnSortedExprs = [UnSortedExpr]
type UnSortedExpr = ([Symbol], Expr)
data MeasureKind
- = MsReflect
- | MsMeasure
- | MsLifted
- | MsClass
- | MsAbsMeasure
- | MsSelector
- | MsChecker
data CMeasure ty = CM {
- cName :: LocSymbol
- cSort :: ty
}
data Def ty ctor = Def {
- measure :: LocSymbol
- ctor :: ctor
- dsort :: Maybe ty
- binds :: [(Symbol, Maybe ty)]
- body :: Body
}
data Body
- = E Expr
- | P Expr
- | R Symbol Expr
data MSpec ty ctor = MSpec {
- ctorMap :: HashMap Symbol [Def ty ctor]
- measMap :: HashMap LocSymbol (Measure ty ctor)
- cmeasMap :: HashMap LocSymbol (Measure ty ())
- imeas :: ![Measure ty ctor]
}
type BScope = Bool
data RClass ty = RClass {
- rcName :: BTyCon
- rcSupers :: [ty]
- rcTyVars :: [BTyVar]
- rcMethods :: [(LocSymbol, ty)]
}
data KVKind
- = RecBindE Var
- | NonRecBindE Var
- | TypeInstE
- | PredInstE
- | LamE
- | CaseE Int
- | LetE
- | ImplictE
- | ProjectE
data KVProf
emptyKVProf :: KVProf
updKVProf :: KVKind -> Kuts -> KVProf -> KVProf
mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a
data LogicMap = LM {
- lmSymDefs :: HashMap Symbol LMap
- lmVarSyms :: HashMap Var (Maybe Symbol)
}
toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap
eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr
data LMap = LMap {
- lmVar :: LocSymbol
- lmArgs :: [Symbol]
- lmExpr :: Expr
}
type RDEnv = DEnv Var SpecType
newtype DEnv x ty = DEnv (HashMap x (HashMap Symbol (RISig ty)))
data RInstance t = RI {
- riclass :: BTyCon
- ritype :: [t]
- risigs :: [(LocSymbol, RISig t)]
}
data RISig t
- = RIAssumed t
- | RISig t
data RILaws ty = RIL {
- rilName :: BTyCon
- rilSupers :: [ty]
- rilTyArgs :: [ty]
- rilEqus :: [(LocSymbol, LocSymbol)]
- rilPos :: Located ()
}
data MethodType t = MT {
- tyInstance :: !(Maybe t)
- tyClass :: !(Maybe t)
}
getMethodType :: MethodType t -> Maybe t
class Reftable r => UReftable r where
- ofUReft :: UReft Reft -> r
liquidBegin :: String
liquidEnd :: String
data Axiom b s e = Axiom {
- aname :: (Var, Maybe DataCon)
- rname :: Maybe b
- abinds :: [b]
- atypes :: [s]
- alhs :: e
- arhs :: e
}
type HAxiom = Axiom Var Type CoreExpr
rtyVarType :: RTyVar -> Type
tyVarVar :: RTVar RTyVar c -> Var

Options

module Language.Haskell.Liquid.UX.Config

Ghc Information

data TargetVars #

Which Top-Level Binders Should be Verified

Constructors

AllVars
Only ![Var]

Instances

Instances details

PPrint TargetVars #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetVars -> Doc # pprintPrec :: Int -> Tidy -> TargetVars -> Doc #

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

Instances details

Qualify TyConMap #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap #

F.Located Things

data Located a #

Constructors

Loc
Fields loc :: !SourcePos locE :: !SourcePos val :: !a

Instances

Instances details

Functor Located
Instance details Defined in Language.Fixpoint.Types.Spans Methods fmap :: (a -> b) -> Located a -> Located b # (<$) :: a -> Located b -> Located a #
Foldable Located
Instance details Defined in Language.Fixpoint.Types.Spans Methods fold :: Monoid m => Located m -> m # foldMap :: Monoid m => (a -> m) -> Located a -> m # foldMap' :: Monoid m => (a -> m) -> Located a -> m # foldr :: (a -> b -> b) -> b -> Located a -> b # foldr' :: (a -> b -> b) -> b -> Located a -> b # foldl :: (b -> a -> b) -> b -> Located a -> b # foldl' :: (b -> a -> b) -> b -> Located a -> b # foldr1 :: (a -> a -> a) -> Located a -> a # foldl1 :: (a -> a -> a) -> Located a -> a # toList :: Located a -> [a] # null :: Located a -> Bool # length :: Located a -> Int # elem :: Eq a => a -> Located a -> Bool # maximum :: Ord a => Located a -> a # minimum :: Ord a => Located a -> a # sum :: Num a => Located a -> a # product :: Num a => Located a -> a #
Traversable Located
Instance details Defined in Language.Fixpoint.Types.Spans Methods traverse :: Applicative f => (a -> f b) -> Located a -> f (Located b) # sequenceA :: Applicative f => Located (f a) -> f (Located a) # mapM :: Monad m => (a -> m b) -> Located a -> m (Located b) # sequence :: Monad m => Located (m a) -> m (Located a) #
TyConable LocSymbol #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: LocSymbol -> Bool # isList :: LocSymbol -> Bool # isTuple :: LocSymbol -> Bool # ppTycon :: LocSymbol -> Doc # isClass :: LocSymbol -> Bool # isEqual :: LocSymbol -> Bool # isNumCls :: LocSymbol -> Bool # isFracCls :: LocSymbol -> Bool #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
Eq a => Eq (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods (==) :: Located a -> Located a -> Bool # (/=) :: Located a -> Located a -> Bool #
Data a => Data (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Located a -> c (Located a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Located a) # toConstr :: Located a -> Constr # dataTypeOf :: Located a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Located a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Located a)) # gmapT :: (forall b. Data b => b -> b) -> Located a -> Located a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQ :: (forall d. Data d => d -> u) -> Located a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Located a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) #
Ord a => Ord (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods compare :: Located a -> Located a -> Ordering # (<) :: Located a -> Located a -> Bool # (<=) :: Located a -> Located a -> Bool # (>) :: Located a -> Located a -> Bool # (>=) :: Located a -> Located a -> Bool # max :: Located a -> Located a -> Located a # min :: Located a -> Located a -> Located a #
Show a => Show (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods showsPrec :: Int -> Located a -> ShowS # show :: Located a -> String # showList :: [Located a] -> ShowS #
IsString a => IsString (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods fromString :: String -> Located a #
Generic (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Associated Types type Rep (Located a) :: Type -> Type # Methods from :: Located a -> Rep (Located a) x # to :: Rep (Located a) x -> Located a #
NFData a => NFData (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods rnf :: Located a -> () #
Binary a => Binary (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Located a -> Put # get :: Get (Located a) # putList :: [Located a] -> Put #
Symbolic a => Symbolic (Located a)
Instance details Defined in Language.Fixpoint.Types.Names Methods symbol :: Located a -> Symbol
Fixpoint a => Fixpoint (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: Located a -> Doc simplify :: Located a -> Located a
PPrint a => PPrint (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> Located a -> Doc # pprintPrec :: Int -> Tidy -> Located a -> Doc #
Expression a => Expression (Located a)
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Located a -> Expr
Subable a => Subable (Located a)
Instance details Defined in Language.Fixpoint.Types.Refinements Methods syms :: Located a -> [Symbol] substa :: (Symbol -> Symbol) -> Located a -> Located a substf :: (Symbol -> Expr) -> Located a -> Located a subst :: Subst -> Located a -> Located a subst1 :: Located a -> (Symbol, Expr) -> Located a
Loc (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: Located a -> SrcSpan
Hashable a => Hashable (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> Located a -> Int hash :: Located a -> Int
Qualify a => Qualify (Located a) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a #
REq r => REq (Located r) #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: Located r -> Located r -> Bool #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
type Rep (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans type Rep (Located a) = D1 ('MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.10.1-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 #

type LocText = Located Text #

Default unknown name

dummyName :: Symbol #

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

Bare Type Constructors and Variables

data BTyCon #

Constructors

BTyCon
Fields btc_tc :: !LocSymbol TyCon name with location information btc_class :: !Bool Is this a class type constructor? btc_prom :: !Bool Is Promoted Data Con?

Instances

Instances details

Eq BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: BTyCon -> BTyCon -> Bool # (/=) :: BTyCon -> BTyCon -> Bool #
Data BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BTyCon -> c BTyCon # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BTyCon # toConstr :: BTyCon -> Constr # dataTypeOf :: BTyCon -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BTyCon) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BTyCon) # gmapT :: (forall b. Data b => b -> b) -> BTyCon -> BTyCon # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BTyCon -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BTyCon -> r # gmapQ :: (forall d. Data d => d -> u) -> BTyCon -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BTyCon -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyCon -> m BTyCon #
Ord BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: BTyCon -> BTyCon -> Ordering # (<) :: BTyCon -> BTyCon -> Bool # (<=) :: BTyCon -> BTyCon -> Bool # (>) :: BTyCon -> BTyCon -> Bool # (>=) :: BTyCon -> BTyCon -> Bool # max :: BTyCon -> BTyCon -> BTyCon # min :: BTyCon -> BTyCon -> BTyCon #
Show BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> BTyCon -> ShowS # show :: BTyCon -> String # showList :: [BTyCon] -> ShowS #
Generic BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep BTyCon :: Type -> Type # Methods from :: BTyCon -> Rep BTyCon x # to :: Rep BTyCon x -> BTyCon #
NFData BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: BTyCon -> () #
Binary BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: BTyCon -> Put # get :: Get BTyCon # putList :: [BTyCon] -> Put #
Symbolic BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: BTyCon -> Symbol
Fixpoint BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: BTyCon -> Doc simplify :: BTyCon -> BTyCon
PPrint BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyCon -> Doc # pprintPrec :: Int -> Tidy -> BTyCon -> Doc #
Loc BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: BTyCon -> SrcSpan
Hashable BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> BTyCon -> Int hash :: BTyCon -> Int
TyConable BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: BTyCon -> Bool # isList :: BTyCon -> Bool # isTuple :: BTyCon -> Bool # ppTycon :: BTyCon -> Doc # isClass :: BTyCon -> Bool # isEqual :: BTyCon -> Bool # isNumCls :: BTyCon -> Bool # isFracCls :: BTyCon -> Bool #
Qualify BareType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
FreeVar BTyCon BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: BTyCon -> [BTyVar]
SubsTy BTyVar BSort BSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort #
SubsTy BTyVar BSort BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon #
SubsTy Symbol Symbol (BRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
Reftable (RTProp BTyCon BTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar () -> Bool ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () toReft :: RTProp BTyCon BTyVar () -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar () params :: RTProp BTyCon BTyVar () -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
Reftable (RType BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]
type Rep BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep BTyCon = D1 ('MetaData "BTyCon" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "BTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "btc_tc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :: (S1 ('MetaSel ('Just "btc_class") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :: S1 ('MetaSel ('Just "btc_prom") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))))

mkBTyCon :: LocSymbol -> BTyCon #

isClassBTyCon :: BTyCon -> Bool #

newtype BTyVar #

Constructors

BTV Symbol

Instances

Instances details

Eq BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: BTyVar -> BTyVar -> Bool # (/=) :: BTyVar -> BTyVar -> Bool #
Data BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BTyVar -> c BTyVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BTyVar # toConstr :: BTyVar -> Constr # dataTypeOf :: BTyVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BTyVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BTyVar) # gmapT :: (forall b. Data b => b -> b) -> BTyVar -> BTyVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r # gmapQ :: (forall d. Data d => d -> u) -> BTyVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BTyVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar #
Ord BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: BTyVar -> BTyVar -> Ordering # (<) :: BTyVar -> BTyVar -> Bool # (<=) :: BTyVar -> BTyVar -> Bool # (>) :: BTyVar -> BTyVar -> Bool # (>=) :: BTyVar -> BTyVar -> Bool # max :: BTyVar -> BTyVar -> BTyVar # min :: BTyVar -> BTyVar -> BTyVar #
Show BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> BTyVar -> ShowS # show :: BTyVar -> String # showList :: [BTyVar] -> ShowS #
IsString BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fromString :: String -> BTyVar #
Generic BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep BTyVar :: Type -> Type # Methods from :: BTyVar -> Rep BTyVar x # to :: Rep BTyVar x -> BTyVar #
NFData BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: BTyVar -> () #
Binary BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: BTyVar -> Put # get :: Get BTyVar # putList :: [BTyVar] -> Put #
Symbolic BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: BTyVar -> Symbol
PPrint BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyVar -> Doc # pprintPrec :: Int -> Tidy -> BTyVar -> Doc #
Hashable BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> BTyVar -> Int hash :: BTyVar -> Int
Qualify BareType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
FreeVar BTyCon BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: BTyCon -> [BTyVar]
SubsTy BTyVar BSort BSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort #
SubsTy BTyVar BSort BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon #
SubsTy Symbol Symbol (BRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r #
SubsTy BTyVar (RType c BTyVar ()) BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
Reftable (RTProp BTyCon BTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar () -> Bool ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () toReft :: RTProp BTyCon BTyVar () -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar () params :: RTProp BTyCon BTyVar () -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
Reftable (RType BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]
type Rep BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep BTyVar

Refined Type Constructors

data RTyCon #

Constructors

RTyCon TyCon ![RPVar] !TyConInfo

Instances

Instances details

Eq RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RTyCon -> RTyCon -> Bool # (/=) :: RTyCon -> RTyCon -> Bool #
Data RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyCon -> c RTyCon # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyCon # toConstr :: RTyCon -> Constr # dataTypeOf :: RTyCon -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyCon) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyCon) # gmapT :: (forall b. Data b => b -> b) -> RTyCon -> RTyCon # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r # gmapQ :: (forall d. Data d => d -> u) -> RTyCon -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyCon -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon #
Show Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Show RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RTyCon -> ShowS # show :: RTyCon -> String # showList :: [RTyCon] -> ShowS #
Generic RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep RTyCon :: Type -> Type # Methods from :: RTyCon -> Rep RTyCon x # to :: Rep RTyCon x -> RTyCon #
Semigroup REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
Monoid REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
NFData RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTyCon -> () #
Exception Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
Symbolic RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: RTyCon -> Symbol
Fixpoint RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: RTyCon -> Doc simplify :: RTyCon -> RTyCon
PPrint Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyCon -> Doc # pprintPrec :: Int -> Tidy -> RTyCon -> Doc #
Hashable RTyCon
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods hashWithSalt :: Int -> RTyCon -> Int hash :: RTyCon -> Int
TyConable RTyCon #	TyConable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: RTyCon -> Bool # isList :: RTyCon -> Bool # isTuple :: RTyCon -> Bool # ppTycon :: RTyCon -> Doc # isClass :: RTyCon -> Bool # isEqual :: RTyCon -> Bool # isNumCls :: RTyCon -> Bool # isFracCls :: RTyCon -> Bool #
Result Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError #
Qualify SpecType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType #
Qualify RTyCon #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon #
REq SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool #
FreeVar RTyCon RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: RTyCon -> [RTyVar]
SubsTy tv RSort Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate #
SubsTy TyVar Type SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType #
SubsTy Symbol RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType #
SubsTy RTyVar RSort PrType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType #
SubsTy RTyVar RSort RSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort #
SubsTy RTyVar RSort RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon #
SubsTy RTyVar RTyVar SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) # true :: RRType r -> m (RRType r) # refresh :: RRType r -> m (RRType r) #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) #
Exception [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods syms :: RRProp Reft -> [Symbol] substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft subst :: Subst -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft
Result [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError #
Qualify (Measure SpecType DataCon) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon #
Reftable (RTProp RTyCon RTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar () -> Bool ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () toReft :: RTProp RTyCon RTyVar () -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar () params :: RTProp RTyCon RTyVar () -> [Symbol]
Reftable (RTProp RTyCon RTyVar Reft)
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft toReft :: RTProp RTyCon RTyVar Reft -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar Reft params :: RTProp RTyCon RTyVar Reft -> [Symbol]
Reftable (RTProp RTyCon RTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType RTyCon RTyVar r -> Bool ppTy :: RType RTyCon RTyVar r -> Doc -> Doc top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r toReft :: RType RTyCon RTyVar r -> Reft ofReft :: Reft -> RType RTyCon RTyVar r params :: RType RTyCon RTyVar r -> [Symbol]
type Rep RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep RTyCon = D1 ('MetaData "RTyCon" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "RTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtc_tc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyCon) :: (S1 ('MetaSel ('Just "rtc_pvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RPVar]) :: S1 ('MetaSel ('Just "rtc_info") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyConInfo))))

data TyConInfo #

Co- and Contra-variance for TyCon --------------------------------

Indexes start from 0 and type or predicate arguments can be both covariant and contravaariant e.g., for the below Foo dataType

data Foo a b c d :: b - Prop, q :: Int -> Prop, r :: a -> Prop> = F (ar -> bp) | Q (c -> a) | G (Intq -> ar)

there will be:

varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant] variancePsArgs = [Covariant, Contravatiant, Bivariant]

Constructors

TyConInfo
Fields varianceTyArgs :: !VarianceInfo variance info for type variables variancePsArgs :: !VarianceInfo variance info for predicate variables sizeFunction :: !(Maybe SizeFun) logical UNARY function that computes the size of the structure

Instances

Instances details

Data TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConInfo -> c TyConInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConInfo # toConstr :: TyConInfo -> Constr # dataTypeOf :: TyConInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConInfo) # gmapT :: (forall b. Data b => b -> b) -> TyConInfo -> TyConInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> TyConInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo #
Show TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> TyConInfo -> ShowS # show :: TyConInfo -> String # showList :: [TyConInfo] -> ShowS #
Generic TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep TyConInfo :: Type -> Type # Methods from :: TyConInfo -> Rep TyConInfo x # to :: Rep TyConInfo x -> TyConInfo #
NFData TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: TyConInfo -> () #
Default TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods def :: TyConInfo
Qualify TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConInfo -> TyConInfo #
type Rep TyConInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "TyConInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "varianceTyArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :: (S1 ('MetaSel ('Just "variancePsArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :: S1 ('MetaSel ('Just "sizeFunction") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun)))))

defaultTyConInfo :: TyConInfo #

rTyConPVs :: RTyCon -> [RPVar] #

rTyConPropVs :: RTyCon -> [PVar RSort] #

isClassType :: TyConable c => RType c t t1 -> Bool #

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

isRVar :: RType c tv r -> Bool #

isBool :: RType RTyCon t t1 -> Bool #

Accessors for RTyCon

Refinement Types

data RType c tv r #

Constructors

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

Instances

Instances details

Show Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Semigroup REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
Monoid REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
Exception Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
PPrint Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
Result Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError #
Qualify SpecType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType #
Qualify BareType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
REq SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool #
SubsTy tv RSort Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate #
SubsTy TyVar Type SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType #
SubsTy Symbol RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType #
SubsTy RTyVar RSort PrType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType #
SubsTy RTyVar RSort RSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort #
SubsTy RTyVar RSort RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon #
SubsTy RTyVar RTyVar SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType #
SubsTy BTyVar BSort BSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort #
SubsTy BTyVar BSort BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon #
SubsTy Symbol Symbol (BRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r #
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) # true :: RRType r -> m (RRType r) # refresh :: RRType r -> m (RRType r) #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar #
SubsTy BTyVar (RType c BTyVar ()) BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) #
Exception [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods syms :: RRProp Reft -> [Symbol] substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft subst :: Subst -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft
Result [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError #
Functor (RType c tv) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RType c tv a -> RType c tv b # (<$) :: a -> RType c tv b -> RType c tv a #
Show tv => Show (RTVU c tv) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RTVU c tv -> ShowS # show :: RTVU c tv -> String # showList :: [RTVU c tv] -> ShowS #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc # pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #
Qualify (Measure SpecType DataCon) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon #
(Eq tv, Eq r, Eq c) => Eq (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RType c tv r -> RType c tv r -> Bool # (/=) :: RType c tv r -> RType c tv r -> Bool #
(Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ())) => Eq (RType c tv ()) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (==) :: RType c tv () -> RType c tv () -> Bool # (/=) :: RType c tv () -> RType c tv () -> Bool #
(Data c, Data tv, Data r) => Data (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> RType c tv r -> c0 (RType c tv r) # gunfold :: (forall b r0. Data b => c0 (b -> r0) -> c0 r0) -> (forall r1. r1 -> c0 r1) -> Constr -> c0 (RType c tv r) # toConstr :: RType c tv r -> Constr # dataTypeOf :: RType c tv r -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (RType c tv r)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (RType c tv r)) # gmapT :: (forall b. Data b => b -> b) -> RType c tv r -> RType c tv r # gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> RType c tv r -> r0 # gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> RType c tv r -> r0 # gmapQ :: (forall d. Data d => d -> u) -> RType c tv r -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RType c tv r -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RType c tv r -> m (RType c tv r) #
PPrint (RTProp c tv r) => Show (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RTProp c tv r -> ShowS # show :: RTProp c tv r -> String # showList :: [RTProp c tv r] -> ShowS #
PPrint (RType c tv r) => Show (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RType c tv r -> ShowS # show :: RType c tv r -> String # showList :: [RType c tv r] -> ShowS #
Generic (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RType c tv r) :: Type -> Type # Methods from :: RType c tv r -> Rep (RType c tv r) x # to :: Rep (RType c tv r) x -> RType c tv r #
(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r # sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r # stimes :: Integral b => b -> RTProp c tv r -> RTProp c tv r #
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (<>) :: RType c tv r -> RType c tv r -> RType c tv r # sconcat :: NonEmpty (RType c tv r) -> RType c tv r # stimes :: Integral b => b -> RType c tv r -> RType c tv r #
(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods mempty :: RTProp c tv r # mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r # mconcat :: [RTProp c tv r] -> RTProp c tv r #
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods mempty :: RType c tv r # mappend :: RType c tv r -> RType c tv r -> RType c tv r # mconcat :: [RType c tv r] -> RType c tv r #
(NFData c, NFData tv, NFData r) => NFData (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RType c tv r -> () #
(Binary c, Binary tv, Binary r) => Binary (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RType c tv r -> Put # get :: Get (RType c tv r) # putList :: [RType c tv r] -> Put #
OkRT c tv r => PPrint (RType c tv r) #	Pretty Printing RefType ---------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RType c tv r -> Doc # pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #
Reftable (RTProp RTyCon RTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar () -> Bool ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () toReft :: RTProp RTyCon RTyVar () -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar () params :: RTProp RTyCon RTyVar () -> [Symbol]
Reftable (RTProp RTyCon RTyVar Reft)
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft toReft :: RTProp RTyCon RTyVar Reft -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar Reft params :: RTProp RTyCon RTyVar Reft -> [Symbol]
Reftable (RTProp RTyCon RTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
Reftable (RTProp BTyCon BTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar () -> Bool ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () toReft :: RTProp BTyCon BTyVar () -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar () params :: RTProp BTyCon BTyVar () -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType RTyCon RTyVar r -> Bool ppTy :: RType RTyCon RTyVar r -> Doc -> Doc top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r toReft :: RType RTyCon RTyVar r -> Reft ofReft :: Reft -> RType RTyCon RTyVar r params :: RType RTyCon RTyVar r -> [Symbol]
Reftable (RType BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]
(Reftable r, TyConable c) => Subable (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: RTProp c tv r -> [Symbol] substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r substf :: (Symbol -> Expr) -> RTProp c tv r -> RTProp c tv r subst :: Subst -> RTProp c tv r -> RTProp c tv r subst1 :: RTProp c tv r -> (Symbol, Expr) -> RTProp c tv r
(Subable r, Reftable r, TyConable c) => Subable (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: RType c tv r -> [Symbol] substa :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r substf :: (Symbol -> Expr) -> RType c tv r -> RType c tv r subst :: Subst -> RType c tv r -> RType c tv r subst1 :: RType c tv r -> (Symbol, Expr) -> RType c tv r
(Hashable tv, Hashable r, Hashable c) => Hashable (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RType c tv r -> Int hash :: RType c tv r -> Int
type Rep (RType c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RType c tv r)

data Ref τ t #

Ref describes `Prop τ` and HProp arguments applied to type constructors. For example, in [a]- v > h}>, we apply (via RApp) * the RProp denoted by `{h -> v > h}` to * the RTyCon denoted by `[]`. Thus, Ref is used for abstract-predicate (arguments) that are associated with _type constructors_ i.e. whose semantics are _dependent upon_ the data-type. In contrast, the Predicate argument in ur_pred in the UReft applies directly to any type and has semantics _independent of_ the data-type.

Constructors

RProp
Fields rf_args :: [(Symbol, τ)] rf_body :: t Abstract refinement associated with `RTyCon`

Instances

Instances details

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r #
Functor (Ref τ) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Ref τ a -> Ref τ b # (<$) :: a -> Ref τ b -> Ref τ a #
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods syms :: RRProp Reft -> [Symbol] substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft subst :: Subst -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft
(Eq τ, Eq t) => Eq (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Ref τ t -> Ref τ t -> Bool # (/=) :: Ref τ t -> Ref τ t -> Bool #
(Data τ, Data t) => Data (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ref τ t -> c (Ref τ t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ref τ t) # toConstr :: Ref τ t -> Constr # dataTypeOf :: Ref τ t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Ref τ t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Ref τ t)) # gmapT :: (forall b. Data b => b -> b) -> Ref τ t -> Ref τ t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ref τ t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ref τ t -> r # gmapQ :: (forall d. Data d => d -> u) -> Ref τ t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ref τ t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ref τ t -> m (Ref τ t) #
Generic (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (Ref τ t) :: Type -> Type # Methods from :: Ref τ t -> Rep (Ref τ t) x # to :: Rep (Ref τ t) x -> Ref τ t #
(NFData τ, NFData t) => NFData (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Ref τ t -> () #
(Binary τ, Binary t) => Binary (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Ref τ t -> Put # get :: Get (Ref τ t) # putList :: [Ref τ t] -> Put #
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc # pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #
(Hashable τ, Hashable t) => Hashable (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Ref τ t -> Int hash :: Ref τ t -> Int
REq t2 => REq (Ref t1 t2) #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: Ref t1 t2 -> Ref t1 t2 -> Bool #
PPrint (RTProp c tv r) => Show (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RTProp c tv r -> ShowS # show :: RTProp c tv r -> String # showList :: [RTProp c tv r] -> ShowS #
(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r # sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r # stimes :: Integral b => b -> RTProp c tv r -> RTProp c tv r #
(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods mempty :: RTProp c tv r # mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r # mconcat :: [RTProp c tv r] -> RTProp c tv r #
Reftable (RTProp RTyCon RTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar () -> Bool ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () toReft :: RTProp RTyCon RTyVar () -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar () params :: RTProp RTyCon RTyVar () -> [Symbol]
Reftable (RTProp RTyCon RTyVar Reft)
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft toReft :: RTProp RTyCon RTyVar Reft -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar Reft params :: RTProp RTyCon RTyVar Reft -> [Symbol]
Reftable (RTProp RTyCon RTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
Reftable (RTProp BTyCon BTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar () -> Bool ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () toReft :: RTProp BTyCon BTyVar () -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar () params :: RTProp BTyCon BTyVar () -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
(Reftable r, TyConable c) => Subable (RTProp c tv r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: RTProp c tv r -> [Symbol] substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r substf :: (Symbol -> Expr) -> RTProp c tv r -> RTProp c tv r subst :: Subst -> RTProp c tv r -> RTProp c tv r subst1 :: RTProp c tv r -> (Symbol, Expr) -> RTProp c tv r
type Rep (Ref τ t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Ref τ t)

type RTProp c tv r = Ref (RType c tv ()) (RType c tv r) #

RTProp is a convenient alias for Ref that will save a bunch of typing. In general, perhaps we need not expose Ref directly at all.

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

newtype RTyVar #

Constructors

RTV TyVar

Instances

Instances details

Eq RTyVar #	Wrappers for GHC Type Elements --------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (==) :: RTyVar -> RTyVar -> Bool # (/=) :: RTyVar -> RTyVar -> Bool #
Data RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyVar -> c RTyVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyVar # toConstr :: RTyVar -> Constr # dataTypeOf :: RTyVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyVar) # gmapT :: (forall b. Data b => b -> b) -> RTyVar -> RTyVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r # gmapQ :: (forall d. Data d => d -> u) -> RTyVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar #
Ord RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods compare :: RTyVar -> RTyVar -> Ordering # (<) :: RTyVar -> RTyVar -> Bool # (<=) :: RTyVar -> RTyVar -> Bool # (>) :: RTyVar -> RTyVar -> Bool # (>=) :: RTyVar -> RTyVar -> Bool # max :: RTyVar -> RTyVar -> RTyVar # min :: RTyVar -> RTyVar -> RTyVar #
Show Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Show RTyVar #	Printing Refinement Types -------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RTyVar -> ShowS # show :: RTyVar -> String # showList :: [RTyVar] -> ShowS #
Generic RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep RTyVar :: Type -> Type # Methods from :: RTyVar -> Rep RTyVar x # to :: Rep RTyVar x -> RTyVar #
Semigroup REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
Monoid REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
NFData RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTyVar -> () #
Exception Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
Symbolic RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: RTyVar -> Symbol
PPrint Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyVar -> Doc # pprintPrec :: Int -> Tidy -> RTyVar -> Doc #
Hashable RTyVar
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods hashWithSalt :: Int -> RTyVar -> Int hash :: RTyVar -> Int
Result Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError #
Qualify SpecType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType #
REq SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool #
FreeVar RTyCon RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: RTyCon -> [RTyVar]
SubsTy tv RSort Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate #
SubsTy TyVar Type SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType #
SubsTy Symbol RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort Sort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort #
SubsTy RTyVar RSort SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType #
SubsTy RTyVar RSort PrType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType #
SubsTy RTyVar RSort RSort #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort #
SubsTy RTyVar RSort RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon #
SubsTy RTyVar RTyVar SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) # true :: RRType r -> m (RRType r) # refresh :: RRType r -> m (RRType r) #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) #
Exception [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods syms :: RRProp Reft -> [Symbol] substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft subst :: Subst -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft
Result [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError #
Qualify (Measure SpecType DataCon) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon #
Reftable (RTProp RTyCon RTyVar ())
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar () -> Bool ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () toReft :: RTProp RTyCon RTyVar () -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar () params :: RTProp RTyCon RTyVar () -> [Symbol]
Reftable (RTProp RTyCon RTyVar Reft)
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft toReft :: RTProp RTyCon RTyVar Reft -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar Reft params :: RTProp RTyCon RTyVar Reft -> [Symbol]
Reftable (RTProp RTyCon RTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType RTyCon RTyVar r -> Bool ppTy :: RType RTyCon RTyVar r -> Doc -> Doc top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r toReft :: RType RTyCon RTyVar r -> Reft ofReft :: Reft -> RType RTyCon RTyVar r params :: RType RTyCon RTyVar r -> [Symbol]
type Rep RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep RTyVar = D1 ('MetaData "RTyVar" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "RTV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyVar)))

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

Instances details

Functor (RTAlias x) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RTAlias x a -> RTAlias x b # (<$) :: a -> RTAlias x b -> RTAlias x a #
(Eq x, Eq a) => Eq (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RTAlias x a -> RTAlias x a -> Bool # (/=) :: RTAlias x a -> RTAlias x a -> Bool #
(Data x, Data a) => Data (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTAlias x a -> c (RTAlias x a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTAlias x a) # toConstr :: RTAlias x a -> Constr # dataTypeOf :: RTAlias x a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTAlias x a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTAlias x a)) # gmapT :: (forall b. Data b => b -> b) -> RTAlias x a -> RTAlias x a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQ :: (forall d. Data d => d -> u) -> RTAlias x a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTAlias x a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) #
(Show tv, Show ty) => Show (RTAlias tv ty) #	Auxiliary Stuff Used Elsewhere ---------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RTAlias tv ty -> ShowS # show :: RTAlias tv ty -> String # showList :: [RTAlias tv ty] -> ShowS #
Generic (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RTAlias x a) :: Type -> Type # Methods from :: RTAlias x a -> Rep (RTAlias x a) x0 # to :: Rep (RTAlias x a) x0 -> RTAlias x a #
(Binary x, Binary a) => Binary (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RTAlias x a -> Put # get :: Get (RTAlias x a) # putList :: [RTAlias x a] -> Put #
(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #
(Hashable x, Hashable a) => Hashable (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RTAlias x a -> Int hash :: RTAlias x a -> Int
type Rep (RTAlias x a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RTAlias x a)

type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv) #

lmapEAlias :: LMap -> Located (RTAlias Symbol Expr) #

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

Worlds

data HSeg t #

Constructors

HBind
Fields hs_addr :: !Symbol hs_val :: t
HVar UsedPVar

Instances

Instances details

Data t => Data (HSeg t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HSeg t -> c (HSeg t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HSeg t) # toConstr :: HSeg t -> Constr # dataTypeOf :: HSeg t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (HSeg t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (HSeg t)) # gmapT :: (forall b. Data b => b -> b) -> HSeg t -> HSeg t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HSeg t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HSeg t -> r # gmapQ :: (forall d. Data d => d -> u) -> HSeg t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HSeg t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HSeg t -> m (HSeg t) #
Generic (HSeg t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (HSeg t) :: Type -> Type # Methods from :: HSeg t -> Rep (HSeg t) x # to :: Rep (HSeg t) x -> HSeg t #
type Rep (HSeg t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (HSeg t)

newtype World t #

A World is a Separation Logic predicate that is essentially a sequence of binders that satisfies two invariants (TODO:LIQUID): 1. Each `hs_addr :: Symbol` appears at most once, 2. There is at most one HVar in a list.

Constructors

World [HSeg t]

Instances

Instances details

Data t => Data (World t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> World t -> c (World t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (World t) # toConstr :: World t -> Constr # dataTypeOf :: World t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (World t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (World t)) # gmapT :: (forall b. Data b => b -> b) -> World t -> World t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> World t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> World t -> r # gmapQ :: (forall d. Data d => d -> u) -> World t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> World t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> World t -> m (World t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> World t -> m (World t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> World t -> m (World t) #
Generic (World t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (World t) :: Type -> Type # Methods from :: World t -> Rep (World t) x # to :: Rep (World t) x -> World t #
type Rep (World t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (World t) = D1 ('MetaData "World" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "World" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HSeg t])))

Classes describing operations on `RTypes`

class Eq c => TyConable c where #

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool #

isList :: c -> Bool #

isTuple :: c -> Bool #

ppTycon :: c -> Doc #

isClass :: c -> Bool #

isEqual :: c -> Bool #

isNumCls :: c -> Bool #

isFracCls :: c -> Bool #

Instances

Instances details

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

class SubsTy tv ty a where #

Methods

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

Instances

Instances details

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

Type Variables

data RTVar tv s #

Constructors

RTVar
Fields ty_var_value :: tv ty_var_info :: RTVInfo s

Instances

Instances details

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) #
Eq tv => Eq (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RTVar tv s -> RTVar tv s -> Bool # (/=) :: RTVar tv s -> RTVar tv s -> Bool #
(Data tv, Data s) => Data (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVar tv s -> c (RTVar tv s) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVar tv s) # toConstr :: RTVar tv s -> Constr # dataTypeOf :: RTVar tv s -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVar tv s)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVar tv s)) # gmapT :: (forall b. Data b => b -> b) -> RTVar tv s -> RTVar tv s # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r # gmapQ :: (forall d. Data d => d -> u) -> RTVar tv s -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVar tv s -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) #
Show tv => Show (RTVU c tv) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RTVU c tv -> ShowS # show :: RTVU c tv -> String # showList :: [RTVU c tv] -> ShowS #
Generic (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RTVar tv s) :: Type -> Type # Methods from :: RTVar tv s -> Rep (RTVar tv s) x # to :: Rep (RTVar tv s) x -> RTVar tv s #
(NFData tv, NFData s) => NFData (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTVar tv s -> () #
(Binary tv, Binary s) => Binary (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RTVar tv s -> Put # get :: Get (RTVar tv s) # putList :: [RTVar tv s] -> Put #
PPrint v => PPrint (RTVar v s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTVar v s -> Doc # pprintPrec :: Int -> Tidy -> RTVar v s -> Doc #
(Hashable tv, Hashable s) => Hashable (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RTVar tv s -> Int hash :: RTVar tv s -> Int
type Rep (RTVar tv s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "RTVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ty_var_value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 tv) :*: S1 ('MetaSel ('Just "ty_var_info") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RTVInfo s))))

data RTVInfo s #

Constructors

RTVNoInfo
Fields rtv_is_pol :: Bool
RTVInfo
Fields rtv_name :: Symbol rtv_kind :: s rtv_is_val :: Bool rtv_is_pol :: Bool

Instances

Instances details

Functor RTVInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RTVInfo a -> RTVInfo b # (<$) :: a -> RTVInfo b -> RTVInfo a #
Data s => Data (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVInfo s -> c (RTVInfo s) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVInfo s) # toConstr :: RTVInfo s -> Constr # dataTypeOf :: RTVInfo s -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVInfo s)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVInfo s)) # gmapT :: (forall b. Data b => b -> b) -> RTVInfo s -> RTVInfo s # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r # gmapQ :: (forall d. Data d => d -> u) -> RTVInfo s -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVInfo s -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) #
Generic (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RTVInfo s) :: Type -> Type # Methods from :: RTVInfo s -> Rep (RTVInfo s) x # to :: Rep (RTVInfo s) x -> RTVInfo s #
NFData s => NFData (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTVInfo s -> () #
Binary s => Binary (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RTVInfo s -> Put # get :: Get (RTVInfo s) # putList :: [RTVInfo s] -> Put #
Hashable s => Hashable (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RTVInfo s -> Int hash :: RTVInfo s -> Int
type Rep (RTVInfo s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RTVInfo s)

makeRTVar :: tv -> RTVar tv s #

mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s #

dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 #

rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s) #

setRtvPol :: RTVar tv a -> Bool -> RTVar tv a #

Predicate Variables

data PVar t #

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

Constructors

PV
Fields pname :: !Symbol ptype :: !(PVKind t) parg :: !Symbol pargs :: ![(t, Symbol, Expr)]

Instances

Instances details

Functor PVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> PVar a -> PVar b # (<$) :: a -> PVar b -> PVar a #
Subable UsedPVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: UsedPVar -> [Symbol] substa :: (Symbol -> Symbol) -> UsedPVar -> UsedPVar substf :: (Symbol -> Expr) -> UsedPVar -> UsedPVar subst :: Subst -> UsedPVar -> UsedPVar subst1 :: UsedPVar -> (Symbol, Expr) -> UsedPVar
SubsTy tv ty ty => SubsTy tv ty (PVar ty) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> PVar ty -> PVar ty #
Eq (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: PVar t -> PVar t -> Bool # (/=) :: PVar t -> PVar t -> Bool #
Data t => Data (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PVar t -> c (PVar t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PVar t) # toConstr :: PVar t -> Constr # dataTypeOf :: PVar t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PVar t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (PVar t)) # gmapT :: (forall b. Data b => b -> b) -> PVar t -> PVar t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PVar t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PVar t -> r # gmapQ :: (forall d. Data d => d -> u) -> PVar t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PVar t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PVar t -> m (PVar t) #
Ord (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: PVar t -> PVar t -> Ordering # (<) :: PVar t -> PVar t -> Bool # (<=) :: PVar t -> PVar t -> Bool # (>) :: PVar t -> PVar t -> Bool # (>=) :: PVar t -> PVar t -> Bool # max :: PVar t -> PVar t -> PVar t # min :: PVar t -> PVar t -> PVar t #
Show t => Show (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> PVar t -> ShowS # show :: PVar t -> String # showList :: [PVar t] -> ShowS #
Generic (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (PVar t) :: Type -> Type # Methods from :: PVar t -> Rep (PVar t) x # to :: Rep (PVar t) x -> PVar t #
NFData t => NFData (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: PVar t -> () #
Binary t => Binary (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: PVar t -> Put # get :: Get (PVar t) # putList :: [PVar t] -> Put #
PPrint (PVar a) #	F.PPrint -----------------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> PVar a -> Doc # pprintPrec :: Int -> Tidy -> PVar a -> Doc #
Hashable (PVar a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> PVar a -> Int hash :: PVar a -> Int
type Rep (PVar t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (PVar t)

isPropPV :: PVar t -> Bool #

pvType :: PVar t -> t #

data PVKind t #

Constructors

PVProp t
PVHProp

Instances

Instances details

Functor PVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> PVKind a -> PVKind b # (<$) :: a -> PVKind b -> PVKind a #
Foldable PVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => PVKind m -> m # foldMap :: Monoid m => (a -> m) -> PVKind a -> m # foldMap' :: Monoid m => (a -> m) -> PVKind a -> m # foldr :: (a -> b -> b) -> b -> PVKind a -> b # foldr' :: (a -> b -> b) -> b -> PVKind a -> b # foldl :: (b -> a -> b) -> b -> PVKind a -> b # foldl' :: (b -> a -> b) -> b -> PVKind a -> b # foldr1 :: (a -> a -> a) -> PVKind a -> a # foldl1 :: (a -> a -> a) -> PVKind a -> a # toList :: PVKind a -> [a] # null :: PVKind a -> Bool # length :: PVKind a -> Int # elem :: Eq a => a -> PVKind a -> Bool # maximum :: Ord a => PVKind a -> a # minimum :: Ord a => PVKind a -> a # sum :: Num a => PVKind a -> a # product :: Num a => PVKind a -> a #
Traversable PVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods traverse :: Applicative f => (a -> f b) -> PVKind a -> f (PVKind b) # sequenceA :: Applicative f => PVKind (f a) -> f (PVKind a) # mapM :: Monad m => (a -> m b) -> PVKind a -> m (PVKind b) # sequence :: Monad m => PVKind (m a) -> m (PVKind a) #
SubsTy tv ty ty => SubsTy tv ty (PVKind ty) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> PVKind ty -> PVKind ty #
Data t => Data (PVKind t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PVKind t -> c (PVKind t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PVKind t) # toConstr :: PVKind t -> Constr # dataTypeOf :: PVKind t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PVKind t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (PVKind t)) # gmapT :: (forall b. Data b => b -> b) -> PVKind t -> PVKind t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PVKind t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PVKind t -> r # gmapQ :: (forall d. Data d => d -> u) -> PVKind t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PVKind t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PVKind t -> m (PVKind t) #
Show t => Show (PVKind t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> PVKind t -> ShowS # show :: PVKind t -> String # showList :: [PVKind t] -> ShowS #
Generic (PVKind t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (PVKind t) :: Type -> Type # Methods from :: PVKind t -> Rep (PVKind t) x # to :: Rep (PVKind t) x -> PVKind t #
NFData a => NFData (PVKind a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: PVKind a -> () #
Binary a => Binary (PVKind a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: PVKind a -> Put # get :: Get (PVKind a) # putList :: [PVKind a] -> Put #
type Rep (PVKind t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (PVKind t) = D1 ('MetaData "PVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "PVProp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "PVHProp" 'PrefixI 'False) (U1 :: Type -> Type))

newtype Predicate #

Constructors

Pr [UsedPVar]

Instances

Instances details

Eq Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Predicate -> Predicate -> Bool # (/=) :: Predicate -> Predicate -> Bool #
Data Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Predicate -> c Predicate # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Predicate # toConstr :: Predicate -> Constr # dataTypeOf :: Predicate -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Predicate) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate) # gmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r # gmapQ :: (forall d. Data d => d -> u) -> Predicate -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Predicate -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #
Show Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods showsPrec :: Int -> Predicate -> ShowS # show :: Predicate -> String # showList :: [Predicate] -> ShowS #
Generic Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep Predicate :: Type -> Type # Methods from :: Predicate -> Rep Predicate x # to :: Rep Predicate x -> Predicate #
Semigroup Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: Predicate -> Predicate -> Predicate # sconcat :: NonEmpty Predicate -> Predicate # stimes :: Integral b => b -> Predicate -> Predicate #
Monoid Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: Predicate # mappend :: Predicate -> Predicate -> Predicate # mconcat :: [Predicate] -> Predicate #
NFData Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Predicate -> () #
Binary Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Predicate -> Put # get :: Get Predicate # putList :: [Predicate] -> Put #
PPrint Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Predicate -> Doc # pprintPrec :: Int -> Tidy -> Predicate -> Doc #
Reftable Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isTauto :: Predicate -> Bool ppTy :: Predicate -> Doc -> Doc top :: Predicate -> Predicate bot :: Predicate -> Predicate meet :: Predicate -> Predicate -> Predicate toReft :: Predicate -> Reft ofReft :: Reft -> Predicate params :: Predicate -> [Symbol]
Subable Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: Predicate -> [Symbol] substa :: (Symbol -> Symbol) -> Predicate -> Predicate substf :: (Symbol -> Expr) -> Predicate -> Predicate subst :: Subst -> Predicate -> Predicate subst1 :: Predicate -> (Symbol, Expr) -> Predicate
Hashable Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Predicate -> Int hash :: Predicate -> Int
SubsTy tv RSort Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate #
SubsTy RTyVar RSort PrType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType #
type Rep Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep Predicate = D1 ('MetaData "Predicate" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'True) (C1 ('MetaCons "Pr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UsedPVar])))

Refinements

data UReft r #

Constructors

MkUReft
Fields ur_reft :: !r ur_pred :: !Predicate

Instances

Instances details

Functor UReft #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> UReft a -> UReft b # (<$) :: a -> UReft b -> UReft a #
Show Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Foldable UReft #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => UReft m -> m # foldMap :: Monoid m => (a -> m) -> UReft a -> m # foldMap' :: Monoid m => (a -> m) -> UReft a -> m # foldr :: (a -> b -> b) -> b -> UReft a -> b # foldr' :: (a -> b -> b) -> b -> UReft a -> b # foldl :: (b -> a -> b) -> b -> UReft a -> b # foldl' :: (b -> a -> b) -> b -> UReft a -> b # foldr1 :: (a -> a -> a) -> UReft a -> a # foldl1 :: (a -> a -> a) -> UReft a -> a # toList :: UReft a -> [a] # null :: UReft a -> Bool # length :: UReft a -> Int # elem :: Eq a => a -> UReft a -> Bool # maximum :: Ord a => UReft a -> a # minimum :: Ord a => UReft a -> a # sum :: Num a => UReft a -> a # product :: Num a => UReft a -> a #
Traversable UReft #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods traverse :: Applicative f => (a -> f b) -> UReft a -> f (UReft b) # sequenceA :: Applicative f => UReft (f a) -> f (UReft a) # mapM :: Monad m => (a -> m b) -> UReft a -> m (UReft b) # sequence :: Monad m => UReft (m a) -> m (UReft a) #
Semigroup REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
Monoid REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
Exception Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
PPrint Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
Result Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError #
Qualify SpecType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType #
Qualify BareType #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType #
Qualify RReft #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Qualify BareSpec #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec #
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
REq SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool #
Freshable m Integer => Freshable m RReft #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m RReft # true :: RReft -> m RReft # refresh :: RReft -> m RReft #
SubsTy TyVar Type SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType #
SubsTy RTyVar RSort SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType #
SubsTy RTyVar RTyVar SpecType #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType #
SubsTy tv ty r => SubsTy tv ty (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> UReft r -> UReft r #
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) #
Eq r => Eq (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: UReft r -> UReft r -> Bool # (/=) :: UReft r -> UReft r -> Bool #
Data r => Data (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UReft r -> c (UReft r) # gunfold :: (forall b r0. Data b => c (b -> r0) -> c r0) -> (forall r1. r1 -> c r1) -> Constr -> c (UReft r) # toConstr :: UReft r -> Constr # dataTypeOf :: UReft r -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (UReft r)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UReft r)) # gmapT :: (forall b. Data b => b -> b) -> UReft r -> UReft r # gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReft r -> r0 # gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReft r -> r0 # gmapQ :: (forall d. Data d => d -> u) -> UReft r -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UReft r -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UReft r -> m (UReft r) #
PPrint (UReft r) => Show (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> UReft r -> ShowS # show :: UReft r -> String # showList :: [UReft r] -> ShowS #
Show (UReft Reft) #
Instance details Defined in Language.Haskell.Liquid.Transforms.RefSplit Methods showsPrec :: Int -> UReft Reft -> ShowS # show :: UReft Reft -> String # showList :: [UReft Reft] -> ShowS #
Generic (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (UReft r) :: Type -> Type # Methods from :: UReft r -> Rep (UReft r) x # to :: Rep (UReft r) x -> UReft r #
Semigroup a => Semigroup (UReft a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: UReft a -> UReft a -> UReft a # sconcat :: NonEmpty (UReft a) -> UReft a # stimes :: Integral b => b -> UReft a -> UReft a #
Monoid a => Monoid (UReft a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: UReft a # mappend :: UReft a -> UReft a -> UReft a # mconcat :: [UReft a] -> UReft a #
NFData r => NFData (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: UReft r -> () #
Binary r => Binary (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: UReft r -> Put # get :: Get (UReft r) # putList :: [UReft r] -> Put #
Exception [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
(PPrint r, Reftable r) => PPrint (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> UReft r -> Doc # pprintPrec :: Int -> Tidy -> UReft r -> Doc #
Expression (UReft ()) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods expr :: UReft () -> Expr
(PPrint r, Reftable r) => Reftable (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isTauto :: UReft r -> Bool ppTy :: UReft r -> Doc -> Doc top :: UReft r -> UReft r bot :: UReft r -> UReft r meet :: UReft r -> UReft r -> UReft r toReft :: UReft r -> Reft ofReft :: Reft -> UReft r params :: UReft r -> [Symbol]
Subable r => Subable (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: UReft r -> [Symbol] substa :: (Symbol -> Symbol) -> UReft r -> UReft r substf :: (Symbol -> Expr) -> UReft r -> UReft r subst :: Subst -> UReft r -> UReft r subst1 :: UReft r -> (Symbol, Expr) -> UReft r
Hashable r => Hashable (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> UReft r -> Int hash :: UReft r -> Int
UReftable (UReft Reft) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods ofUReft :: UReft Reft -> UReft Reft #
Result [Error] #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError #
REq (UReft Reft) #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: UReft Reft -> UReft Reft -> Bool #
Binary (Spec LocBareType LocSymbol) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
Qualify (Measure SpecType DataCon) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon #
Reftable (RTProp RTyCon RTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
Reftable (RType BTyCon BTyVar (UReft Reft))
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]
type Rep (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (UReft r) = D1 ('MetaData "UReft" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "MkUReft" 'PrefixI 'True) (S1 ('MetaSel ('Just "ur_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 r) :*: S1 ('MetaSel ('Just "ur_pred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Predicate)))

Parse-time entities describing refined data types

data SizeFun #

Termination expressions

Constructors

IdSizeFun	x -> F.EVar x
SymSizeFun LocSymbol	x -> f x

Instances

Instances details

Data SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SizeFun -> c SizeFun # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SizeFun # toConstr :: SizeFun -> Constr # dataTypeOf :: SizeFun -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SizeFun) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SizeFun) # gmapT :: (forall b. Data b => b -> b) -> SizeFun -> SizeFun # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SizeFun -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SizeFun -> r # gmapQ :: (forall d. Data d => d -> u) -> SizeFun -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SizeFun -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFun -> m SizeFun #
Show SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> SizeFun -> ShowS # show :: SizeFun -> String # showList :: [SizeFun] -> ShowS #
Generic SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep SizeFun :: Type -> Type # Methods from :: SizeFun -> Rep SizeFun x # to :: Rep SizeFun x -> SizeFun #
NFData SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: SizeFun -> () #
Binary SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: SizeFun -> Put # get :: Get SizeFun # putList :: [SizeFun] -> Put #
PPrint SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> SizeFun -> Doc # pprintPrec :: Int -> Tidy -> SizeFun -> Doc #
Hashable SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> SizeFun -> Int hash :: SizeFun -> Int
Qualify SizeFun #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun #
type Rep SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep SizeFun = D1 ('MetaData "SizeFun" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "IdSizeFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SymSizeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol)))

szFun :: SizeFun -> Symbol -> Expr #

data DataDecl #

Data type refinements

Constructors

DataDecl
Fields tycName :: DataName Type Constructor Name tycTyVars :: [Symbol] Tyvar Parameters tycPVars :: [PVar BSort] PVar Parameters tycDCons :: [DataCtor] Data Constructors tycSrcPos :: !SourcePos Source Position tycSFun :: Maybe SizeFun Default termination measure tycPropTy :: Maybe BareType Type of Ind-Prop tycKind :: !DataDeclKind User-defined or Auto-lifted

Instances

Instances details

Eq DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataDecl -> DataDecl -> Bool # (/=) :: DataDecl -> DataDecl -> Bool #
Data DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDecl -> c DataDecl # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDecl # toConstr :: DataDecl -> Constr # dataTypeOf :: DataDecl -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDecl) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDecl) # gmapT :: (forall b. Data b => b -> b) -> DataDecl -> DataDecl # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDecl -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDecl -> r # gmapQ :: (forall d. Data d => d -> u) -> DataDecl -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDecl -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDecl -> m DataDecl #
Ord DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: DataDecl -> DataDecl -> Ordering # (<) :: DataDecl -> DataDecl -> Bool # (<=) :: DataDecl -> DataDecl -> Bool # (>) :: DataDecl -> DataDecl -> Bool # (>=) :: DataDecl -> DataDecl -> Bool # max :: DataDecl -> DataDecl -> DataDecl # min :: DataDecl -> DataDecl -> DataDecl #
Show DataDecl #	For debugging.
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataDecl -> ShowS # show :: DataDecl -> String # showList :: [DataDecl] -> ShowS #
Generic DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep DataDecl :: Type -> Type # Methods from :: DataDecl -> Rep DataDecl x # to :: Rep DataDecl x -> DataDecl #
Binary DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataDecl -> Put # get :: Get DataDecl # putList :: [DataDecl] -> Put #
Symbolic DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: DataDecl -> Symbol
PPrint DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
Loc DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataDecl -> SrcSpan
Hashable DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataDecl -> Int hash :: DataDecl -> Int
Qualify DataDecl #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl #
type Rep DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataDecl

data DataName #

The name of the TyCon corresponding to a DataDecl

Constructors

DnName !LocSymbol	for `isVanillyAlgTyCon` we can directly use the `TyCon` name
DnCon !LocSymbol	for `FamInst` TyCon we save some `DataCon` name

Instances

Instances details

Eq DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataName -> DataName -> Bool # (/=) :: DataName -> DataName -> Bool #
Data DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataName -> c DataName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataName # toConstr :: DataName -> Constr # dataTypeOf :: DataName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataName) # gmapT :: (forall b. Data b => b -> b) -> DataName -> DataName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataName -> r # gmapQ :: (forall d. Data d => d -> u) -> DataName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataName -> m DataName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataName -> m DataName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataName -> m DataName #
Ord DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: DataName -> DataName -> Ordering # (<) :: DataName -> DataName -> Bool # (<=) :: DataName -> DataName -> Bool # (>) :: DataName -> DataName -> Bool # (>=) :: DataName -> DataName -> Bool # max :: DataName -> DataName -> DataName # min :: DataName -> DataName -> DataName #
Show DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataName -> ShowS # show :: DataName -> String # showList :: [DataName] -> ShowS #
Generic DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep DataName :: Type -> Type # Methods from :: DataName -> Rep DataName x # to :: Rep DataName x -> DataName #
Binary DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataName -> Put # get :: Get DataName # putList :: [DataName] -> Put #
Symbolic DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: DataName -> Symbol
PPrint DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataName -> Doc # pprintPrec :: Int -> Tidy -> DataName -> Doc #
Loc DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataName -> SrcSpan
Hashable DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataName -> Int hash :: DataName -> Int
type Rep DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataName = D1 ('MetaData "DataName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "DnName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol)) :+: C1 ('MetaCons "DnCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol)))

dataNameSymbol :: DataName -> LocSymbol #

data DataCtor #

Data Constructor

Constructors

DataCtor
Fields dcName :: LocSymbol DataCon name dcTyVars :: [Symbol] Type parameters dcTheta :: [BareType] The GHC ThetaType corresponding to DataCon.dataConSig dcFields :: [(Symbol, BareType)] field-name and field-Type pairs dcResult :: Maybe BareType Possible output (if in GADT form)

Instances

Instances details

Data DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataCtor -> c DataCtor # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataCtor # toConstr :: DataCtor -> Constr # dataTypeOf :: DataCtor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataCtor) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCtor) # gmapT :: (forall b. Data b => b -> b) -> DataCtor -> DataCtor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataCtor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataCtor -> r # gmapQ :: (forall d. Data d => d -> u) -> DataCtor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataCtor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCtor -> m DataCtor #
Generic DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep DataCtor :: Type -> Type # Methods from :: DataCtor -> Rep DataCtor x # to :: Rep DataCtor x -> DataCtor #
Binary DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataCtor -> Put # get :: Get DataCtor # putList :: [DataCtor] -> Put #
PPrint DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
Loc DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataCtor -> SrcSpan
Hashable DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataCtor -> Int hash :: DataCtor -> Int
Qualify DataCtor #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor #
type Rep DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataCtor

data DataConP #

Constructors

DataConP

Fields

dcpLoc :: !SourcePos
dcpCon :: !DataCon
Corresponding GHC DataCon
dcpFreeTyVars :: ![RTyVar]
Type parameters
dcpFreePred :: ![PVar RSort]
Abstract Refinement parameters
dcpTyConstrs :: ![SpecType]
? Class constraints (via dataConStupidTheta)
dcpTyArgs :: ![(Symbol, SpecType)]
Value parameters
dcpTyRes :: !SpecType
Result type , tyData :: !SpecType -- ^ The generic ADT, see [NOTE:DataCon-Data]
dcpIsGadt :: !Bool
Was this specified in GADT style (if so, DONT use function names as fields)
dcpModule :: !Symbol
Which module was this defined in
dcpLocE :: !SourcePos

Instances

Instances details

Data DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataConP -> c DataConP # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataConP # toConstr :: DataConP -> Constr # dataTypeOf :: DataConP -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataConP) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataConP) # gmapT :: (forall b. Data b => b -> b) -> DataConP -> DataConP # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataConP -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataConP -> r # gmapQ :: (forall d. Data d => d -> u) -> DataConP -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataConP -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConP -> m DataConP #
Show DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods showsPrec :: Int -> DataConP -> ShowS # show :: DataConP -> String # showList :: [DataConP] -> ShowS #
Generic DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep DataConP :: Type -> Type # Methods from :: DataConP -> Rep DataConP x # to :: Rep DataConP x -> DataConP #
PPrint DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> DataConP -> Doc # pprintPrec :: Int -> Tidy -> DataConP -> Doc #
Loc DataConP #	NOTE:DataCon-Data for each `DataConP` we also store the type of the constructed data. This is the same as `tyRes` for vanilla ADTs (e.g. List, Maybe etc.) but may differ for GADTs. For example, data Thing a where X :: Thing Int Y :: Thing Bool Here the `DataConP` associated with `X` (resp. `Y`) has `tyRes` corresponding to 'Thing Int' (resp. 'Thing Bool'), but in both cases, the `tyData` should be 'Thing a'.
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataConP -> SrcSpan
type Rep DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataConP

data HasDataDecl #

Constructors

NoDecl (Maybe SizeFun)
HasDecl

Instances

Instances details

Show HasDataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> HasDataDecl -> ShowS # show :: HasDataDecl -> String # showList :: [HasDataDecl] -> ShowS #
PPrint HasDataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc #

hasDecl :: DataDecl -> HasDataDecl #

data DataDeclKind #

What kind of DataDecl is it?

Constructors

DataUser	User defined data-definitions (should have refined fields)
DataReflected	Automatically lifted data-definitions (do not have refined fields)

Instances

Instances details

Eq DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataDeclKind -> DataDeclKind -> Bool # (/=) :: DataDeclKind -> DataDeclKind -> Bool #
Data DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDeclKind -> c DataDeclKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDeclKind # toConstr :: DataDeclKind -> Constr # dataTypeOf :: DataDeclKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDeclKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDeclKind) # gmapT :: (forall b. Data b => b -> b) -> DataDeclKind -> DataDeclKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclKind -> r # gmapQ :: (forall d. Data d => d -> u) -> DataDeclKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDeclKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclKind -> m DataDeclKind #
Show DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataDeclKind -> ShowS # show :: DataDeclKind -> String # showList :: [DataDeclKind] -> ShowS #
Generic DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep DataDeclKind :: Type -> Type # Methods from :: DataDeclKind -> Rep DataDeclKind x # to :: Rep DataDeclKind x -> DataDeclKind #
NFData DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: DataDeclKind -> () #
Binary DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataDeclKind -> Put # get :: Get DataDeclKind # putList :: [DataDeclKind] -> Put #
Hashable DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataDeclKind -> Int hash :: DataDeclKind -> Int
type Rep DataDeclKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataDeclKind = D1 ('MetaData "DataDeclKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "DataUser" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataReflected" 'PrefixI 'False) (U1 :: Type -> Type))

data TyConP #

Constructors

TyConP
Fields tcpLoc :: !SourcePos tcpCon :: !TyCon tcpFreeTyVarsTy :: ![RTyVar] tcpFreePredTy :: ![PVar RSort] tcpVarianceTs :: !VarianceInfo tcpVariancePs :: !VarianceInfo tcpSizeFun :: !(Maybe SizeFun)

Instances

Instances details

Data TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConP -> c TyConP # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConP # toConstr :: TyConP -> Constr # dataTypeOf :: TyConP -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConP) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConP) # gmapT :: (forall b. Data b => b -> b) -> TyConP -> TyConP # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r # gmapQ :: (forall d. Data d => d -> u) -> TyConP -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConP -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP #
Show TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods showsPrec :: Int -> TyConP -> ShowS # show :: TyConP -> String # showList :: [TyConP] -> ShowS #
Generic TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep TyConP :: Type -> Type # Methods from :: TyConP -> Rep TyConP x # to :: Rep TyConP x -> TyConP #
PPrint TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> TyConP -> Doc # pprintPrec :: Int -> Tidy -> TyConP -> Doc #
Loc TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: TyConP -> SrcSpan
Qualify TyConP #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP #
type Rep TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun))))))

Pre-instantiated RType

type RRType #

Arguments

= RType RTyCon RTyVar

Resolved version

type RRProp r = Ref RSort (RRType r) #

type BRType #

Arguments

= RType BTyCon BTyVar

Bare parsed version

type BRProp r = Ref BSort (BRType r) #

type BSort = BRType () #

type BPVar = PVar BSort #

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

Unified Representation of Refinement Types --------------------------------

type PVU c tv = PVar (RType c tv ()) #

Instantiated RType

type BareType = BRType RReft #

type PrType = RRType Predicate #

type SpecType = RRType RReft #

type SpecProp = RRProp RReft #

type SpecRTVar = RTVar RTyVar RSort #

type SpecRep = RRep RReft #

type LocBareType = Located BareType #

type LocSpecType = Located SpecType #

type RSort = RRType () #

type UsedPVar = PVar () #

Predicates ----------------------------------------------------------------

type RPVar = PVar RSort #

type RReft = UReft Reft #

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

Instances details

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

Constructing & Destructing RTypes

data RTypeRep c tv r #

Constructor and Destructors for RTypes ------------------------------------

Constructors

RTypeRep
Fields ty_vars :: [(RTVar tv (RType c tv ()), r)] ty_preds :: [PVar (RType c tv ())] ty_ebinds :: [Symbol] ty_erefts :: [r] ty_eargs :: [RType c tv r] ty_binds :: [Symbol] ty_refts :: [r] ty_args :: [RType c tv r] ty_res :: RType c tv r

fromRTypeRep :: RTypeRep c tv r -> RType c tv r #

toRTypeRep :: RType c tv r -> RTypeRep c tv r #

mkArrow :: [(RTVar tv (RType c tv ()), r)] -> [PVar (RType c tv ())] -> [(Symbol, RType c tv r, r)] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv r #

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

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

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

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

bkUniv :: RType tv c r -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())], RType tv c r) #

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

bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])], SpecType) #

rImpF :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r #

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

rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r #

rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r #

Manipulating `Predicates`

pvars :: Predicate -> [UsedPVar] #

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

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

Some tests on RTypes

isBase :: RType t t1 t2 -> Bool #

isFunTy :: RType t t1 t2 -> Bool #

isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool #

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

Traversing `RType`

efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b #

foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a #

foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a #

emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType c tv r1 -> RType c tv r2 #

mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2 #

mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2) #

mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r) #

mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft #

Visitors ------------------------------------------------------------------

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

mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r #

foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc #

???

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

Instances details

Eq Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods (==) :: Oblig -> Oblig -> Bool # (/=) :: Oblig -> Oblig -> Bool #
Data Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Oblig -> c Oblig # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Oblig # toConstr :: Oblig -> Constr # dataTypeOf :: Oblig -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Oblig) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig) # gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Oblig -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #
Show Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods showsPrec :: Int -> Oblig -> ShowS # show :: Oblig -> String # showList :: [Oblig] -> ShowS #
Generic Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Associated Types type Rep Oblig :: Type -> Type # Methods from :: Oblig -> Rep Oblig x # to :: Rep Oblig x -> Oblig #
NFData Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods rnf :: Oblig -> () #
Binary Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods put :: Oblig -> Put # get :: Get Oblig # putList :: [Oblig] -> Put #
PPrint Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> Oblig -> Doc # pprintPrec :: Int -> Tidy -> Oblig -> Doc #
Hashable Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods hashWithSalt :: Int -> Oblig -> Int hash :: Oblig -> Int
type Rep Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.1-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 #

addInvCond :: SpecType -> RReft -> SpecType #

Inferred Annotations

newtype AnnInfo a #

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

Constructors

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

Instances

Instances details

Functor AnnInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> AnnInfo a -> AnnInfo b # (<$) :: a -> AnnInfo b -> AnnInfo a #
Data a => Data (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnInfo a -> c (AnnInfo a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AnnInfo a) # toConstr :: AnnInfo a -> Constr # dataTypeOf :: AnnInfo a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AnnInfo a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AnnInfo a)) # gmapT :: (forall b. Data b => b -> b) -> AnnInfo a -> AnnInfo a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQ :: (forall d. Data d => d -> u) -> AnnInfo a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnInfo a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) #
PPrint a => Show (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods showsPrec :: Int -> AnnInfo a -> ShowS # show :: AnnInfo a -> String # showList :: [AnnInfo a] -> ShowS #
Generic (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (AnnInfo a) :: Type -> Type # Methods from :: AnnInfo a -> Rep (AnnInfo a) x # to :: Rep (AnnInfo a) x -> AnnInfo a #
Semigroup (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: AnnInfo a -> AnnInfo a -> AnnInfo a # sconcat :: NonEmpty (AnnInfo a) -> AnnInfo a # stimes :: Integral b => b -> AnnInfo a -> AnnInfo a #
Monoid (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: AnnInfo a # mappend :: AnnInfo a -> AnnInfo a -> AnnInfo a # mconcat :: [AnnInfo a] -> AnnInfo a #
NFData a => NFData (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: AnnInfo a -> () #
PPrint a => PPrint (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> AnnInfo a -> Doc # pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #
FromJSON a => FromJSON (AnnInfo a)
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods parseJSON :: Value -> Parser (AnnInfo a) parseJSONList :: Value -> Parser [AnnInfo a]
ToJSON a => ToJSON (AnnInfo a)
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods toJSON :: AnnInfo a -> Value toEncoding :: AnnInfo a -> Encoding toJSONList :: [AnnInfo a] -> Value toEncodingList :: [AnnInfo a] -> Encoding
type Rep (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (AnnInfo a) = D1 ('MetaData "AnnInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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

Instances details

Functor Annot #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Annot a -> Annot b # (<$) :: a -> Annot b -> Annot a #
Data t => Data (Annot t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot t -> c (Annot t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Annot t) # toConstr :: Annot t -> Constr # dataTypeOf :: Annot t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Annot t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Annot t)) # gmapT :: (forall b. Data b => b -> b) -> Annot t -> Annot t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQ :: (forall d. Data d => d -> u) -> Annot t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) #
Generic (Annot t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (Annot t) :: Type -> Type # Methods from :: Annot t -> Rep (Annot t) x # to :: Rep (Annot t) x -> Annot t #
NFData a => NFData (Annot a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Annot a -> () #
PPrint t => PPrint (Annot t) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Annot t -> Doc # pprintPrec :: Int -> Tidy -> Annot t -> Doc #
type Rep (Annot t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Annot t) = D1 ('MetaData "Annot" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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

Instances details

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

Overall Output

data Output a #

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

Constructors

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

Instances

Instances details

Functor Output #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Output a -> Output b # (<$) :: a -> Output b -> Output a #
Generic (Output a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (Output a) :: Type -> Type # Methods from :: Output a -> Rep (Output a) x # to :: Rep (Output a) x -> Output a #
Semigroup (Output a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: Output a -> Output a -> Output a # sconcat :: NonEmpty (Output a) -> Output a # stimes :: Integral b => b -> Output a -> Output a #
Monoid (Output a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: Output a # mappend :: Output a -> Output a -> Output a # mconcat :: [Output a] -> Output a #
FromJSON (Output Doc)
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods parseJSON :: Value -> Parser (Output Doc) parseJSONList :: Value -> Parser [Output Doc]
ToJSON (Output Doc)
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods toJSON :: Output Doc -> Value toEncoding :: Output Doc -> Encoding toJSONList :: [Output Doc] -> Value toEncodingList :: [Output Doc] -> Encoding
type Rep (Output a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Output a) = D1 ('MetaData "Output" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 :: Expr #

isHole :: Expr -> Bool #

hasHoleTy :: RType t t1 t2 -> Bool #

Converting To and From Sort

ofRSort :: Reftable r => RType c tv () -> RType c tv r #

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

rTypeValueVar :: Reftable r => RType c tv r -> Symbol #

rTypeReft :: Reftable r => RType c tv r -> Reft #

stripRTypeBase :: RType c tv r -> Maybe r #

topRTypeBase :: Reftable r => RType c tv r -> RType c tv r #

Class for values that can be pretty printed

class PPrint a where #

Minimal complete definition

Nothing

Methods

pprintTidy :: Tidy -> a -> Doc #

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

Instances

Instances details

PPrint Bool
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Bool -> Doc # pprintPrec :: Int -> Tidy -> Bool -> Doc #
PPrint Float
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Float -> Doc # pprintPrec :: Int -> Tidy -> Float -> Doc #
PPrint Int
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Int -> Doc # pprintPrec :: Int -> Tidy -> Int -> Doc #
PPrint Integer
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Integer -> Doc # pprintPrec :: Int -> Tidy -> Integer -> Doc #
PPrint ()
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> () -> Doc # pprintPrec :: Int -> Tidy -> () -> Doc #
PPrint Doc
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Doc -> Doc # pprintPrec :: Int -> Tidy -> Doc -> Doc #
PPrint SourceError #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> SourceError -> Doc # pprintPrec :: Int -> Tidy -> SourceError -> Doc #
PPrint AltCon #
Instance details Defined in Language.Haskell.Liquid.Synthesize.Misc Methods pprintTidy :: Tidy -> AltCon -> Doc # pprintPrec :: Int -> Tidy -> AltCon -> Doc #
PPrint Class #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Class -> Doc # pprintPrec :: Int -> Tidy -> Class -> Doc #
PPrint DataCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #
PPrint Type #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Type -> Doc # pprintPrec :: Int -> Tidy -> Type -> Doc #
PPrint TyThing #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> TyThing -> Doc # pprintPrec :: Int -> Tidy -> TyThing -> Doc #
PPrint Var #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Var -> Doc # pprintPrec :: Int -> Tidy -> Var -> Doc #
PPrint ErrMsg #	A whole bunch of PPrint instances follow ----------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> ErrMsg -> Doc # pprintPrec :: Int -> Tidy -> ErrMsg -> Doc #
PPrint SrcSpan #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> SrcSpan -> Doc # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #
PPrint TyCon #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> TyCon -> Doc # pprintPrec :: Int -> Tidy -> TyCon -> Doc #
PPrint Name #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Name -> Doc # pprintPrec :: Int -> Tidy -> Name -> Doc #
PPrint ParseError #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> ParseError -> Doc # pprintPrec :: Int -> Tidy -> ParseError -> Doc #
PPrint Text
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Text -> Doc # pprintPrec :: Int -> Tidy -> Text -> Doc #
PPrint AxiomEnv
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> AxiomEnv -> Doc # pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc #
PPrint Equation
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Equation -> Doc # pprintPrec :: Int -> Tidy -> Equation -> Doc #
PPrint GFixSolution
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc #
PPrint QualParam
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualParam -> Doc # pprintPrec :: Int -> Tidy -> QualParam -> Doc #
PPrint QualPattern
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualPattern -> Doc # pprintPrec :: Int -> Tidy -> QualPattern -> Doc #
PPrint Qualifier
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Qualifier -> Doc # pprintPrec :: Int -> Tidy -> Qualifier -> Doc #
PPrint Rewrite
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Rewrite -> Doc # pprintPrec :: Int -> Tidy -> Rewrite -> Doc #
PPrint IBindEnv
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> IBindEnv -> Doc # pprintPrec :: Int -> Tidy -> IBindEnv -> Doc #
PPrint Packs
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> Packs -> Doc # pprintPrec :: Int -> Tidy -> Packs -> Doc #
PPrint Error
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint Error1
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error1 -> Doc # pprintPrec :: Int -> Tidy -> Error1 -> Doc #
PPrint Symbol
Instance details Defined in Language.Fixpoint.Types.Names Methods pprintTidy :: Tidy -> Symbol -> Doc # pprintPrec :: Int -> Tidy -> Symbol -> Doc #
PPrint DocTable
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> DocTable -> Doc # pprintPrec :: Int -> Tidy -> DocTable -> Doc #
PPrint Tidy #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Tidy -> Doc # pprintPrec :: Int -> Tidy -> Tidy -> Doc #
PPrint Bop
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Bop -> Doc # pprintPrec :: Int -> Tidy -> Bop -> Doc #
PPrint Brel
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc # pprintPrec :: Int -> Tidy -> Brel -> Doc #
PPrint Constant
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc # pprintPrec :: Int -> Tidy -> Constant -> Doc #
PPrint Expr
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Expr -> Doc # pprintPrec :: Int -> Tidy -> Expr -> Doc #
PPrint KVSub
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVSub -> Doc # pprintPrec :: Int -> Tidy -> KVSub -> Doc #
PPrint KVar
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc # pprintPrec :: Int -> Tidy -> KVar -> Doc #
PPrint Subst
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Subst -> Doc # pprintPrec :: Int -> Tidy -> Subst -> Doc #
PPrint SymConst
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc # pprintPrec :: Int -> Tidy -> SymConst -> Doc #
PPrint DataCtor
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
PPrint DataDecl
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
PPrint DataField
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataField -> Doc # pprintPrec :: Int -> Tidy -> DataField -> Doc #
PPrint FTycon
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> FTycon -> Doc # pprintPrec :: Int -> Tidy -> FTycon -> Doc #
PPrint TCArgs
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> TCArgs -> Doc # pprintPrec :: Int -> Tidy -> TCArgs -> Doc #
PPrint SrcSpan
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SrcSpan -> Doc # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #
PPrint Templates
Instance details Defined in Language.Fixpoint.Types.Templates Methods pprintTidy :: Tidy -> Templates -> Doc # pprintPrec :: Int -> Tidy -> Templates -> Doc #
PPrint Sem
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> Sem -> Doc # pprintPrec :: Int -> Tidy -> Sem -> Doc #
PPrint SmtSort
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> SmtSort -> Doc # pprintPrec :: Int -> Tidy -> SmtSort -> Doc #
PPrint TheorySymbol
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> TheorySymbol -> Doc # pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc #
PPrint Trigger
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Trigger -> Doc # pprintPrec :: Int -> Tidy -> Trigger -> Doc #
PPrint Variance #
Instance details Defined in Language.Haskell.Liquid.Types.Variance Methods pprintTidy :: Tidy -> Variance -> Doc # pprintPrec :: Int -> Tidy -> Variance -> Doc #
PPrint QBind
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> QBind -> Doc # pprintPrec :: Int -> Tidy -> QBind -> Doc #
PPrint Cube
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> Cube -> Doc # pprintPrec :: Int -> Tidy -> Cube -> Doc #
PPrint EbindSol
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EbindSol -> Doc # pprintPrec :: Int -> Tidy -> EbindSol -> Doc #
PPrint Command
Instance details Defined in Language.Fixpoint.Smt.Types Methods pprintTidy :: Tidy -> Command -> Doc # pprintPrec :: Int -> Tidy -> Command -> Doc #
PPrint CVertex
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> CVertex -> Doc # pprintPrec :: Int -> Tidy -> CVertex -> Doc #
PPrint KVGraph
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> KVGraph -> Doc # pprintPrec :: Int -> Tidy -> KVGraph -> Doc #
PPrint Rank
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> Rank -> Doc # pprintPrec :: Int -> Tidy -> Rank -> Doc #
PPrint BIndex
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BIndex -> Doc # pprintPrec :: Int -> Tidy -> BIndex -> Doc #
PPrint BindPred
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BindPred -> Doc # pprintPrec :: Int -> Tidy -> BindPred -> Doc #
PPrint EQual
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EQual -> Doc # pprintPrec :: Int -> Tidy -> EQual -> Doc #
PPrint KIndex
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> KIndex -> Doc # pprintPrec :: Int -> Tidy -> KIndex -> Doc #
PPrint UserError #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> UserError -> Doc # pprintPrec :: Int -> Tidy -> UserError -> Doc #
PPrint Oblig #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> Oblig -> Doc # pprintPrec :: Int -> Tidy -> Oblig -> Doc #
PPrint KVProf #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVProf -> Doc # pprintPrec :: Int -> Tidy -> KVProf -> Doc #
PPrint KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVKind -> Doc # pprintPrec :: Int -> Tidy -> KVKind -> Doc #
PPrint Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Body -> Doc # pprintPrec :: Int -> Tidy -> Body -> Doc #
PPrint ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> ModName -> Doc # pprintPrec :: Int -> Tidy -> ModName -> Doc #
PPrint Error #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint HasDataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc #
PPrint SizeFun #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> SizeFun -> Doc # pprintPrec :: Int -> Tidy -> SizeFun -> Doc #
PPrint DataCtor #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
PPrint DataName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataName -> Doc # pprintPrec :: Int -> Tidy -> DataName -> Doc #
PPrint DataDecl #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
PPrint RTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyCon -> Doc # pprintPrec :: Int -> Tidy -> RTyCon -> Doc #
PPrint BTyCon #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyCon -> Doc # pprintPrec :: Int -> Tidy -> BTyCon -> Doc #
PPrint RTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyVar -> Doc # pprintPrec :: Int -> Tidy -> RTyVar -> Doc #
PPrint BTyVar #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyVar -> Doc # pprintPrec :: Int -> Tidy -> BTyVar -> Doc #
PPrint Predicate #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Predicate -> Doc # pprintPrec :: Int -> Tidy -> Predicate -> Doc #
PPrint TargetVars #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetVars -> Doc # pprintPrec :: Int -> Tidy -> TargetVars -> Doc #
PPrint DataConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> DataConP -> Doc # pprintPrec :: Int -> Tidy -> DataConP -> Doc #
PPrint TyConP #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> TyConP -> Doc # pprintPrec :: Int -> Tidy -> TyConP -> Doc #
PPrint LMap #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LMap -> Doc # pprintPrec :: Int -> Tidy -> LMap -> Doc #
PPrint LogicMap #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LogicMap -> Doc # pprintPrec :: Int -> Tidy -> LogicMap -> Doc #
PPrint Pattern #
Instance details Defined in Language.Haskell.Liquid.GHC.Resugar Methods pprintTidy :: Tidy -> Pattern -> Doc # pprintPrec :: Int -> Tidy -> Pattern -> Doc #
PPrint TargetSpec #	Pretty Printing -----------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetSpec -> Doc # pprintPrec :: Int -> Tidy -> TargetSpec -> Doc #
PPrint TargetInfo #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetInfo -> Doc # pprintPrec :: Int -> Tidy -> TargetInfo -> Doc #
PPrint DiffCheck #
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods pprintTidy :: Tidy -> DiffCheck -> Doc # pprintPrec :: Int -> Tidy -> DiffCheck -> Doc #
PPrint CGInfo #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGInfo -> Doc # pprintPrec :: Int -> Tidy -> CGInfo -> Doc #
PPrint WfC #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> WfC -> Doc # pprintPrec :: Int -> Tidy -> WfC -> Doc #
PPrint SubC #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> SubC -> Doc # pprintPrec :: Int -> Tidy -> SubC -> Doc #
PPrint CGEnv #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGEnv -> Doc # pprintPrec :: Int -> Tidy -> CGEnv -> Doc #
PPrint Stats
Instance details Defined in Language.Fixpoint.Utils.Statistics Methods pprintTidy :: Tidy -> Stats -> Doc # pprintPrec :: Int -> Tidy -> Stats -> Doc #
PPrint a => PPrint [a]
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> [a] -> Doc # pprintPrec :: Int -> Tidy -> [a] -> Doc #
PPrint a => PPrint (Maybe a)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Maybe a -> Doc # pprintPrec :: Int -> Tidy -> Maybe a -> Doc #
PPrint (Expr Var) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Expr Var -> Doc # pprintPrec :: Int -> Tidy -> Expr Var -> Doc #
PPrint (Bind Var) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Bind Var -> Doc # pprintPrec :: Int -> Tidy -> Bind Var -> Doc #
Fixpoint a => PPrint (SimpC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> SimpC a -> Doc # pprintPrec :: Int -> Tidy -> SimpC a -> Doc #
Fixpoint a => PPrint (SubC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> SubC a -> Doc # pprintPrec :: Int -> Tidy -> SubC a -> Doc #
Fixpoint a => PPrint (WfC a)
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> WfC a -> Doc # pprintPrec :: Int -> Tidy -> WfC a -> Doc #
PPrint a => PPrint (SEnv a)
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> SEnv a -> Doc # pprintPrec :: Int -> Tidy -> SEnv a -> Doc #
PPrint a => PPrint (SizedEnv a)
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> SizedEnv a -> Doc # pprintPrec :: Int -> Tidy -> SizedEnv a -> Doc #
PPrint a => PPrint (Located a)
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> Located a -> Doc # pprintPrec :: Int -> Tidy -> Located a -> Doc #
PPrint a => PPrint (Triggered a)
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Triggered a -> Doc # pprintPrec :: Int -> Tidy -> Triggered a -> Doc #
PPrint a => PPrint (HashSet a)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> HashSet a -> Doc # pprintPrec :: Int -> Tidy -> HashSet a -> Doc #
PPrint (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.
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError Doc -> Doc # pprintPrec :: Int -> Tidy -> CtxError Doc -> Doc #
PPrint (CtxError SpecType) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
PPrint t => PPrint (Annot t) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Annot t -> Doc # pprintPrec :: Int -> Tidy -> Annot t -> Doc #
PPrint a => PPrint (AnnInfo a) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> AnnInfo a -> Doc # pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #
PPrint t => PPrint (RClass t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RClass t -> Doc # pprintPrec :: Int -> Tidy -> RClass t -> Doc #
PPrint t => PPrint (CMeasure t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> CMeasure t -> Doc # pprintPrec :: Int -> Tidy -> CMeasure t -> Doc #
PPrint t => PPrint (AREnv t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> AREnv t -> Doc # pprintPrec :: Int -> Tidy -> AREnv t -> Doc #
PPrint t => PPrint (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RISig t -> Doc # pprintPrec :: Int -> Tidy -> RISig t -> Doc #
PPrint t => PPrint (RILaws t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RILaws t -> Doc # pprintPrec :: Int -> Tidy -> RILaws t -> Doc #
PPrint t => PPrint (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RInstance t -> Doc # pprintPrec :: Int -> Tidy -> RInstance t -> Doc #
(PPrint r, Reftable r) => PPrint (UReft r) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> UReft r -> Doc # pprintPrec :: Int -> Tidy -> UReft r -> Doc #
PPrint (PVar a) #	F.PPrint -----------------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> PVar a -> Doc # pprintPrec :: Int -> Tidy -> PVar a -> Doc #
(Show v, PPrint v) => PPrint (PlugTV v) #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods pprintTidy :: Tidy -> PlugTV v -> Doc # pprintPrec :: Int -> Tidy -> PlugTV v -> Doc #
(PPrint a, PPrint b) => PPrint (Either a b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Either a b -> Doc # pprintPrec :: Int -> Tidy -> Either a b -> Doc #
(PPrint a, PPrint b) => PPrint (a, b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b) -> Doc # pprintPrec :: Int -> Tidy -> (a, b) -> Doc #
(PPrint a, PPrint b) => PPrint (HashMap a b)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> HashMap a b -> Doc # pprintPrec :: Int -> Tidy -> HashMap a b -> Doc #
(PPrint a, PPrint b) => PPrint (Sol a b)
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> Sol a b -> Doc # pprintPrec :: Int -> Tidy -> Sol a b -> Doc #
(PPrint t, PPrint a) => PPrint (MSpec t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MSpec t a -> Doc # pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #
PPrint t => PPrint (HoleInfo i t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HoleInfo i t -> Doc # pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #
(PPrint t, PPrint a) => PPrint (Measure t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Measure t a -> Doc # pprintPrec :: Int -> Tidy -> Measure t a -> Doc #
PPrint a => PPrint (Def t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Def t a -> Doc # pprintPrec :: Int -> Tidy -> Def t a -> Doc #
(PPrint tv, PPrint t) => PPrint (RTEnv tv t) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTEnv tv t -> Doc # pprintPrec :: Int -> Tidy -> RTEnv tv t -> Doc #
(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Ref t (RType c tv r) -> Doc # pprintPrec :: Int -> Tidy -> Ref t (RType c tv r) -> Doc #
PPrint v => PPrint (RTVar v s) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTVar v s -> Doc # pprintPrec :: Int -> Tidy -> RTVar v s -> Doc #
(PPrint e, PPrint t) => PPrint (Bound t e) #
Instance details Defined in Language.Haskell.Liquid.Types.Bounds Methods pprintTidy :: Tidy -> Bound t e -> Doc # pprintPrec :: Int -> Tidy -> Bound t e -> Doc #
(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods pprintTidy :: Tidy -> Spec ty bndr -> Doc # pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #
(PPrint ty, PPrint ctor) => PPrint (Pspec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Parse Methods pprintTidy :: Tidy -> Pspec ty ctor -> Doc # pprintPrec :: Int -> Tidy -> Pspec ty ctor -> Doc #
(PPrint a, PPrint b, PPrint c) => PPrint (a, b, c)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c) -> Doc #
OkRT c tv r => PPrint (RType c tv r) #	Pretty Printing RefType ---------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RType c tv r -> Doc # pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #
(PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d) -> Doc #
(PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e)
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d, e) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d, e) -> Doc #

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

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

Printer Configuration

data PPEnv #

Printer ----------------------------------------------------------------

Constructors

PP
Fields ppPs :: Bool print abstract-predicates ppTyVar :: Bool print the unique suffix for each tyvar ppShort :: Bool print the tycons without qualification ppDebug :: Bool gross with full info

Instances

Instances details

Show PPEnv #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> PPEnv -> ShowS # show :: PPEnv -> String # showList :: [PPEnv] -> ShowS #

ppEnv :: PPEnv #

ppEnvShort :: PPEnv -> PPEnv #

Modules and Imports

data ModName #

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

Constructors

ModName !ModType !ModuleName

Instances

Instances details

Eq ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: ModName -> ModName -> Bool # (/=) :: ModName -> ModName -> Bool #
Data ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModName -> c ModName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModName # toConstr :: ModName -> Constr # dataTypeOf :: ModName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModName) # gmapT :: (forall b. Data b => b -> b) -> ModName -> ModName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQ :: (forall d. Data d => d -> u) -> ModName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName #
Ord ModName #
Instance details 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 #
Show ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> ModName -> ShowS # show :: ModName -> String # showList :: [ModName] -> ShowS #
Generic ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep ModName :: Type -> Type # Methods from :: ModName -> Rep ModName x # to :: Rep ModName x -> ModName #
Symbolic ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: ModName -> Symbol
PPrint ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> ModName -> Doc # pprintPrec :: Int -> Tidy -> ModName -> Doc #
Hashable ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> ModName -> Int hash :: ModName -> Int
Qualify ModSpecs #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs #
type Rep ModName #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep ModName = D1 ('MetaData "ModName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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

Instances details

Eq ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: ModType -> ModType -> Bool # (/=) :: ModType -> ModType -> Bool #
Data ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModType -> c ModType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModType # toConstr :: ModType -> Constr # dataTypeOf :: ModType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModType) # gmapT :: (forall b. Data b => b -> b) -> ModType -> ModType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQ :: (forall d. Data d => d -> u) -> ModType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType #
Ord ModType #
Instance details 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 #
Show ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> ModType -> ShowS # show :: ModType -> String # showList :: [ModType] -> ShowS #
Generic ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep ModType :: Type -> Type # Methods from :: ModType -> Rep ModType x # to :: Rep ModType x -> ModType #
Hashable ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> ModType -> Int hash :: ModType -> Int
type Rep ModType #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 #

qualifyModName :: ModName -> Symbol -> Symbol #

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

Instances details

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

type BareRTEnv = RTEnv Symbol BareType #

type SpecRTEnv = RTEnv RTyVar SpecType #

type BareRTAlias = RTAlias Symbol BareType #

type SpecRTAlias = RTAlias RTyVar SpecType #

Diagnostics, Warnings, Errors and Error Messages

module Language.Haskell.Liquid.Types.Errors

type Error = TError SpecType #

type ErrorResult = FixResult UserError #

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

data Warning #

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

Instances

Instances details

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

mkWarning :: SrcSpan -> Doc -> Warning #

data Diagnostics #

Instances

Instances details

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

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

emptyDiagnostics :: Diagnostics #

noErrors :: Diagnostics -> Bool #

allWarnings :: Diagnostics -> [Warning] #

allErrors :: Diagnostics -> [Error] #

printWarning :: DynFlags -> 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

Instances details

Eq Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Cinfo -> Cinfo -> Bool # (/=) :: Cinfo -> Cinfo -> Bool #
Ord Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods compare :: Cinfo -> Cinfo -> Ordering # (<) :: Cinfo -> Cinfo -> Bool # (<=) :: Cinfo -> Cinfo -> Bool # (>) :: Cinfo -> Cinfo -> Bool # (>=) :: Cinfo -> Cinfo -> Bool # max :: Cinfo -> Cinfo -> Cinfo # min :: Cinfo -> Cinfo -> Cinfo #
Show Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Cinfo -> ShowS # show :: Cinfo -> String # showList :: [Cinfo] -> ShowS #
Generic Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep Cinfo :: Type -> Type # Methods from :: Cinfo -> Rep Cinfo x # to :: Rep Cinfo x -> Cinfo #
NFData Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Cinfo -> () #
Fixpoint Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: Cinfo -> Doc simplify :: Cinfo -> Cinfo
Loc Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: Cinfo -> SrcSpan
Result (FixResult Cinfo) #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: FixResult Cinfo -> FixResult UserError #
type Rep Cinfo #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep Cinfo = D1 ('MetaData "Cinfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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

data Measure ty ctor #

Constructors

M
Fields msName :: LocSymbol msSort :: ty msEqns :: [Def ty ctor] msKind :: !MeasureKind msUnSorted :: !UnSortedExprs

Instances

Instances details

Bifunctor Measure #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods bimap :: (a -> b) -> (c -> d) -> Measure a c -> Measure b d # first :: (a -> b) -> Measure a c -> Measure b c # second :: (b -> c) -> Measure a b -> Measure a c #
Qualify BareMeasure #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure #
Functor (Measure ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Measure ty a -> Measure ty b # (<$) :: a -> Measure ty b -> Measure ty a #
(Eq ty, Eq ctor) => Eq (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Measure ty ctor -> Measure ty ctor -> Bool # (/=) :: Measure ty ctor -> Measure ty ctor -> Bool #
(Data ty, Data ctor) => Data (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Measure ty ctor -> c (Measure ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Measure ty ctor) # toConstr :: Measure ty ctor -> Constr # dataTypeOf :: Measure ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Measure ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Measure ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> Measure ty ctor -> Measure ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Measure ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Measure ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> Measure ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Measure ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Measure ty ctor -> m (Measure ty ctor) #
PPrint (Measure t a) => Show (Measure t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Measure t a -> ShowS # show :: Measure t a -> String # showList :: [Measure t a] -> ShowS #
Generic (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (Measure ty ctor) :: Type -> Type # Methods from :: Measure ty ctor -> Rep (Measure ty ctor) x # to :: Rep (Measure ty ctor) x -> Measure ty ctor #
(Binary t, Binary c) => Binary (Measure t c) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Measure t c -> Put # get :: Get (Measure t c) # putList :: [Measure t c] -> Put #
(PPrint t, PPrint a) => PPrint (Measure t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Measure t a -> Doc # pprintPrec :: Int -> Tidy -> Measure t a -> Doc #
Subable (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: Measure ty ctor -> [Symbol] substa :: (Symbol -> Symbol) -> Measure ty ctor -> Measure ty ctor substf :: (Symbol -> Expr) -> Measure ty ctor -> Measure ty ctor subst :: Subst -> Measure ty ctor -> Measure ty ctor subst1 :: Measure ty ctor -> (Symbol, Expr) -> Measure ty ctor
Loc (Measure a b) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: Measure a b -> SrcSpan
(Hashable ty, Hashable ctor) => Hashable (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Measure ty ctor -> Int hash :: Measure ty ctor -> Int
Qualify (Measure SpecType DataCon) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon #
type Rep (Measure ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Measure ty ctor) = D1 ('MetaData "Measure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Def ty ctor]) :: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs)))))

type UnSortedExprs = [UnSortedExpr] #

type UnSortedExpr = ([Symbol], Expr) #

data MeasureKind #

Constructors

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

Instances

Instances details

Eq MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: MeasureKind -> MeasureKind -> Bool # (/=) :: MeasureKind -> MeasureKind -> Bool #
Data MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MeasureKind -> c MeasureKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MeasureKind # toConstr :: MeasureKind -> Constr # dataTypeOf :: MeasureKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MeasureKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MeasureKind) # gmapT :: (forall b. Data b => b -> b) -> MeasureKind -> MeasureKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r # gmapQ :: (forall d. Data d => d -> u) -> MeasureKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MeasureKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind #
Ord MeasureKind #
Instance details 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 #
Show MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MeasureKind -> ShowS # show :: MeasureKind -> String # showList :: [MeasureKind] -> ShowS #
Generic MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep MeasureKind :: Type -> Type # Methods from :: MeasureKind -> Rep MeasureKind x # to :: Rep MeasureKind x -> MeasureKind #
Binary MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: MeasureKind -> Put # get :: Get MeasureKind # putList :: [MeasureKind] -> Put #
Hashable MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> MeasureKind -> Int hash :: MeasureKind -> Int
type Rep MeasureKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep MeasureKind = D1 ('MetaData "MeasureKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 :: LocSymbol cSort :: ty

Instances

Instances details

Functor CMeasure #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> CMeasure a -> CMeasure b # (<$) :: a -> CMeasure b -> CMeasure a #
Data ty => Data (CMeasure ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMeasure ty -> c (CMeasure ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CMeasure ty) # toConstr :: CMeasure ty -> Constr # dataTypeOf :: CMeasure ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CMeasure ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CMeasure ty)) # gmapT :: (forall b. Data b => b -> b) -> CMeasure ty -> CMeasure ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQ :: (forall d. Data d => d -> u) -> CMeasure ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CMeasure ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) #
PPrint (CMeasure t) => Show (CMeasure t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> CMeasure t -> ShowS # show :: CMeasure t -> String # showList :: [CMeasure t] -> ShowS #
Generic (CMeasure ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (CMeasure ty) :: Type -> Type # Methods from :: CMeasure ty -> Rep (CMeasure ty) x # to :: Rep (CMeasure ty) x -> CMeasure ty #
PPrint t => PPrint (CMeasure t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> CMeasure t -> Doc # pprintPrec :: Int -> Tidy -> CMeasure t -> Doc #
type Rep (CMeasure ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)))

data Def ty ctor #

Constructors

Def
Fields measure :: LocSymbol ctor :: ctor dsort :: Maybe ty binds :: [(Symbol, Maybe ty)] body :: Body

Instances

Instances details

Bifunctor Def #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods bimap :: (a -> b) -> (c -> d) -> Def a c -> Def b d # first :: (a -> b) -> Def a c -> Def b c # second :: (b -> c) -> Def a b -> Def a c #
Functor (Def ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Def ty a -> Def ty b # (<$) :: a -> Def ty b -> Def ty a #
(Eq ctor, Eq ty) => Eq (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Def ty ctor -> Def ty ctor -> Bool # (/=) :: Def ty ctor -> Def ty ctor -> Bool #
(Data ty, Data ctor) => Data (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Def ty ctor -> c (Def ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Def ty ctor) # toConstr :: Def ty ctor -> Constr # dataTypeOf :: Def ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Def ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Def ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> Def ty ctor -> Def ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Def ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Def ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> Def ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Def ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Def ty ctor -> m (Def ty ctor) #
(Show ctor, Show ty) => Show (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Def ty ctor -> ShowS # show :: Def ty ctor -> String # showList :: [Def ty ctor] -> ShowS #
Generic (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (Def ty ctor) :: Type -> Type # Methods from :: Def ty ctor -> Rep (Def ty ctor) x # to :: Rep (Def ty ctor) x -> Def ty ctor #
(Binary t, Binary c) => Binary (Def t c) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Def t c -> Put # get :: Get (Def t c) # putList :: [Def t c] -> Put #
PPrint a => PPrint (Def t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Def t a -> Doc # pprintPrec :: Int -> Tidy -> Def t a -> Doc #
Subable (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: Def ty ctor -> [Symbol] substa :: (Symbol -> Symbol) -> Def ty ctor -> Def ty ctor substf :: (Symbol -> Expr) -> Def ty ctor -> Def ty ctor subst :: Subst -> Def ty ctor -> Def ty ctor subst1 :: Def ty ctor -> (Symbol, Expr) -> Def ty ctor
(Hashable ctor, Hashable ty) => Hashable (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Def ty ctor -> Int hash :: Def ty ctor -> Int
Qualify (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor #
type Rep (Def ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Def ty ctor)

data Body #

Measures

Constructors

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

Instances

Instances details

Eq Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Body -> Body -> Bool # (/=) :: Body -> Body -> Bool #
Data Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Body -> c Body # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Body # toConstr :: Body -> Constr # dataTypeOf :: Body -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Body) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Body) # gmapT :: (forall b. Data b => b -> b) -> Body -> Body # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Body -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Body -> r # gmapQ :: (forall d. Data d => d -> u) -> Body -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Body -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Body -> m Body # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Body -> m Body # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Body -> m Body #
Show Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Body -> ShowS # show :: Body -> String # showList :: [Body] -> ShowS #
Generic Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep Body :: Type -> Type # Methods from :: Body -> Rep Body x # to :: Rep Body x -> Body #
Binary Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Body -> Put # get :: Get Body # putList :: [Body] -> Put #
PPrint Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Body -> Doc # pprintPrec :: Int -> Tidy -> Body -> Doc #
Subable Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods syms :: Body -> [Symbol] substa :: (Symbol -> Symbol) -> Body -> Body substf :: (Symbol -> Expr) -> Body -> Body subst :: Subst -> Body -> Body subst1 :: Body -> (Symbol, Expr) -> Body
Hashable Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Body -> Int hash :: Body -> Int
Qualify Body #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body #
type Rep Body #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep Body

data MSpec ty ctor #

Constructors

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

Instances

Instances details

Bifunctor MSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d # first :: (a -> b) -> MSpec a c -> MSpec b c # second :: (b -> c) -> MSpec a b -> MSpec a c #
Functor (MSpec ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> MSpec ty a -> MSpec ty b # (<$) :: a -> MSpec ty b -> MSpec ty a #
(Data ty, Data ctor) => Data (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) # toConstr :: MSpec ty ctor -> Constr # dataTypeOf :: MSpec ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #
(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MSpec ty ctor -> ShowS # show :: MSpec ty ctor -> String # showList :: [MSpec ty ctor] -> ShowS #
Generic (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (MSpec ty ctor) :: Type -> Type # Methods from :: MSpec ty ctor -> Rep (MSpec ty ctor) x # to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #
Eq ctor => Semigroup (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor # sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor # stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #
Eq ctor => Monoid (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: MSpec ty ctor # mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor # mconcat :: [MSpec ty ctor] -> MSpec ty ctor #
(PPrint t, PPrint a) => PPrint (MSpec t a) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MSpec t a -> Doc # pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #
type Rep (MSpec ty ctor) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (MSpec ty ctor)

Scoping Info

type BScope = Bool #

Information about scope Binders Scope in

Type Classes

data RClass ty #

Constructors

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

Instances

Instances details

Functor RClass #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RClass a -> RClass b # (<$) :: a -> RClass b -> RClass a #
Eq ty => Eq (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RClass ty -> RClass ty -> Bool # (/=) :: RClass ty -> RClass ty -> Bool #
Data ty => Data (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RClass ty -> c (RClass ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RClass ty) # toConstr :: RClass ty -> Constr # dataTypeOf :: RClass ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RClass ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RClass ty)) # gmapT :: (forall b. Data b => b -> b) -> RClass ty -> RClass ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQ :: (forall d. Data d => d -> u) -> RClass ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RClass ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) #
Show ty => Show (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RClass ty -> ShowS # show :: RClass ty -> String # showList :: [RClass ty] -> ShowS #
Generic (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RClass ty) :: Type -> Type # Methods from :: RClass ty -> Rep (RClass ty) x # to :: Rep (RClass ty) x -> RClass ty #
Binary ty => Binary (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RClass ty -> Put # get :: Get (RClass ty) # putList :: [RClass ty] -> Put #
PPrint t => PPrint (RClass t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RClass t -> Doc # pprintPrec :: Int -> Tidy -> RClass t -> Doc #
Hashable ty => Hashable (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RClass ty -> Int hash :: RClass ty -> Int
type Rep (RClass ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 [(LocSymbol, 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
ImplictE
ProjectE	Projecting out field of

Instances

Instances details

Eq KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: KVKind -> KVKind -> Bool # (/=) :: KVKind -> KVKind -> Bool #
Data KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVKind -> c KVKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVKind # toConstr :: KVKind -> Constr # dataTypeOf :: KVKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVKind) # gmapT :: (forall b. Data b => b -> b) -> KVKind -> KVKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQ :: (forall d. Data d => d -> u) -> KVKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KVKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind #
Ord KVKind #
Instance details 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 #
Show KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> KVKind -> ShowS # show :: KVKind -> String # showList :: [KVKind] -> ShowS #
Generic KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep KVKind :: Type -> Type # Methods from :: KVKind -> Rep KVKind x # to :: Rep KVKind x -> KVKind #
NFData KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: KVKind -> () #
PPrint KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVKind -> Doc # pprintPrec :: Int -> Tidy -> KVKind -> Doc #
Hashable KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> KVKind -> Int hash :: KVKind -> Int
type Rep KVKind #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep KVKind = D1 ('MetaData "KVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 "ImplictE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjectE" 'PrefixI 'False) (U1 :: Type -> Type)))))

data KVProf #

Instances

Instances details

Generic KVProf #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep KVProf :: Type -> Type # Methods from :: KVProf -> Rep KVProf x # to :: Rep KVProf x -> KVProf #
NFData KVProf #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: KVProf -> () #
PPrint KVProf #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVProf -> Doc # pprintPrec :: Int -> Tidy -> KVProf -> Doc #
type Rep KVProf #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep KVProf = D1 ('MetaData "KVProf" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 #

insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a #

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

Instances details

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

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

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

data LMap #

Constructors

LMap
Fields lmVar :: LocSymbol lmArgs :: [Symbol] lmExpr :: Expr

Instances

Instances details

Show LMap #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> LMap -> ShowS # show :: LMap -> String # showList :: [LMap] -> ShowS #
PPrint LMap #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LMap -> Doc # pprintPrec :: Int -> Tidy -> LMap -> Doc #

Refined Instances

type RDEnv = DEnv Var SpecType #

newtype DEnv x ty #

Constructors

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

Instances

Instances details

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

data RInstance t #

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

Constructors

RI
Fields riclass :: BTyCon ritype :: [t] risigs :: [(LocSymbol, RISig t)]

Instances

Instances details

Functor RInstance #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RInstance a -> RInstance b # (<$) :: a -> RInstance b -> RInstance a #
Eq t => Eq (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RInstance t -> RInstance t -> Bool # (/=) :: RInstance t -> RInstance t -> Bool #
Data t => Data (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RInstance t -> c (RInstance t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RInstance t) # toConstr :: RInstance t -> Constr # dataTypeOf :: RInstance t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RInstance t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RInstance t)) # gmapT :: (forall b. Data b => b -> b) -> RInstance t -> RInstance t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQ :: (forall d. Data d => d -> u) -> RInstance t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RInstance t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) #
Show t => Show (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RInstance t -> ShowS # show :: RInstance t -> String # showList :: [RInstance t] -> ShowS #
Generic (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RInstance t) :: Type -> Type # Methods from :: RInstance t -> Rep (RInstance t) x # to :: Rep (RInstance t) x -> RInstance t #
Binary t => Binary (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RInstance t -> Put # get :: Get (RInstance t) # putList :: [RInstance t] -> Put #
PPrint t => PPrint (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RInstance t -> Doc # pprintPrec :: Int -> Tidy -> RInstance t -> Doc #
Hashable t => Hashable (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RInstance t -> Int hash :: RInstance t -> Int
type Rep (RInstance t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "RI" 'PrefixI 'True) (S1 ('MetaSel ('Just "riclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :: (S1 ('MetaSel ('Just "ritype") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :: S1 ('MetaSel ('Just "risigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, RISig t)]))))

data RISig t #

Constructors

RIAssumed t
RISig t

Instances

Instances details

Functor RISig #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RISig a -> RISig b # (<$) :: a -> RISig b -> RISig a #
Eq t => Eq (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RISig t -> RISig t -> Bool # (/=) :: RISig t -> RISig t -> Bool #
Data t => Data (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RISig t -> c (RISig t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RISig t) # toConstr :: RISig t -> Constr # dataTypeOf :: RISig t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RISig t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RISig t)) # gmapT :: (forall b. Data b => b -> b) -> RISig t -> RISig t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQ :: (forall d. Data d => d -> u) -> RISig t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RISig t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) #
Show t => Show (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RISig t -> ShowS # show :: RISig t -> String # showList :: [RISig t] -> ShowS #
Generic (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RISig t) :: Type -> Type # Methods from :: RISig t -> Rep (RISig t) x # to :: Rep (RISig t) x -> RISig t #
Binary t => Binary (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RISig t -> Put # get :: Get (RISig t) # putList :: [RISig t] -> Put #
PPrint t => PPrint (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RISig t -> Doc # pprintPrec :: Int -> Tidy -> RISig t -> Doc #
Hashable t => Hashable (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RISig t -> Int hash :: RISig t -> Int
type Rep (RISig t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RISig t) = D1 ('MetaData "RISig" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-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 RILaws ty #

Constructors

RIL
Fields rilName :: BTyCon rilSupers :: [ty] rilTyArgs :: [ty] rilEqus :: [(LocSymbol, LocSymbol)] rilPos :: Located ()

Instances

Instances details

Functor RILaws #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> RILaws a -> RILaws b # (<$) :: a -> RILaws b -> RILaws a #
Eq ty => Eq (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RILaws ty -> RILaws ty -> Bool # (/=) :: RILaws ty -> RILaws ty -> Bool #
Data ty => Data (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RILaws ty -> c (RILaws ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RILaws ty) # toConstr :: RILaws ty -> Constr # dataTypeOf :: RILaws ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RILaws ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RILaws ty)) # gmapT :: (forall b. Data b => b -> b) -> RILaws ty -> RILaws ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RILaws ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RILaws ty -> r # gmapQ :: (forall d. Data d => d -> u) -> RILaws ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RILaws ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RILaws ty -> m (RILaws ty) #
Show ty => Show (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RILaws ty -> ShowS # show :: RILaws ty -> String # showList :: [RILaws ty] -> ShowS #
Generic (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (RILaws ty) :: Type -> Type # Methods from :: RILaws ty -> Rep (RILaws ty) x # to :: Rep (RILaws ty) x -> RILaws ty #
Binary t => Binary (RILaws t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: RILaws t -> Put # get :: Get (RILaws t) # putList :: [RILaws t] -> Put #
PPrint t => PPrint (RILaws t) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RILaws t -> Doc # pprintPrec :: Int -> Tidy -> RILaws t -> Doc #
Hashable ty => Hashable (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RILaws ty -> Int hash :: RILaws ty -> Int
type Rep (RILaws ty) #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RILaws ty) = D1 ('MetaData "RILaws" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "RIL" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rilName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :: S1 ('MetaSel ('Just "rilSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :: (S1 ('MetaSel ('Just "rilTyArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty]) :: (S1 ('MetaSel ('Just "rilEqus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, LocSymbol)]) :: S1 ('MetaSel ('Just "rilPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located ()))))))

data MethodType t #

Constructors

MT
Fields tyInstance :: !(Maybe t) tyClass :: !(Maybe t)

Instances

Instances details

Show t => Show (MethodType t) #
Instance details 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 #

Ureftable Instances

class Reftable r => UReftable r where #

Minimal complete definition

Nothing

Methods

ofUReft :: UReft Reft -> r #

Instances

Instances details

UReftable () #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods ofUReft :: UReft Reft -> () #
UReftable (UReft Reft) #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods ofUReft :: UReft Reft -> UReft Reft #

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

Instances details

Show (Axiom Var Type CoreExpr) #
Instance details 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 #

rtyVarType :: RTyVar -> Type #

tyVarVar :: RTVar RTyVar c -> Var #

Orphan instances

Ord DataCon #
Instance details 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 #
Instance details Methods compare :: TyCon -> TyCon -> Ordering # (<) :: TyCon -> TyCon -> Bool # (<=) :: TyCon -> TyCon -> Bool # (>) :: TyCon -> TyCon -> Bool # (>=) :: TyCon -> TyCon -> Bool # max :: TyCon -> TyCon -> TyCon # min :: TyCon -> TyCon -> TyCon #
Show DataCon #
Instance details Methods showsPrec :: Int -> DataCon -> ShowS # show :: DataCon -> String # showList :: [DataCon] -> ShowS #
Show ModuleName #
Instance details Methods showsPrec :: Int -> ModuleName -> ShowS # show :: ModuleName -> String # showList :: [ModuleName] -> ShowS #
Symbolic DataCon #
Instance details Methods symbol :: DataCon -> Symbol
Symbolic ModuleName #
Instance details Methods symbol :: ModuleName -> Symbol
PPrint DataCon #
Instance details Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #
PPrint TyThing #
Instance details Methods pprintTidy :: Tidy -> TyThing -> Doc # pprintPrec :: Int -> Tidy -> TyThing -> Doc #
Hashable ModuleName #
Instance details Methods hashWithSalt :: Int -> ModuleName -> Int hash :: ModuleName -> Int
NFData a => NFData (TError a) #
Instance details Methods rnf :: TError a -> () #
Subable t => Subable (WithModel t) #
Instance details Methods syms :: WithModel t -> [Symbol] substa :: (Symbol -> Symbol) -> WithModel t -> WithModel t substf :: (Symbol -> Expr) -> WithModel t -> WithModel t subst :: Subst -> WithModel t -> WithModel t subst1 :: WithModel t -> (Symbol, Expr) -> WithModel t

Options

Ghc Information

Instances

Instances

F.Located Things

Instances

Symbols

Default unknown name

Bare Type Constructors and Variables

Instances

Instances

Refined Type Constructors

Instances

Instances

Refinement Types

Instances

Instances

Instances

Instances

Worlds

Instances

Instances

Classes describing operations on RTypes

Instances

Instances

Type Variables

Instances

Instances

Predicate Variables

Instances

Instances

Instances

Refinements

Instances

Parse-time entities describing refined data types

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Pre-instantiated RType

Instantiated RType

Instances

Constructing & Destructing RTypes

Manipulating Predicates

Some tests on RTypes

Traversing RType

???

Instances

Inferred Annotations

Instances

Instances

Hole Information

Instances

Overall Output

Instances

Refinement Hole

Converting To and From Sort

Class for values that can be pretty printed

Instances

Printer Configuration

Instances

Modules and Imports

Instances

Instances

Refinement Type Aliases

Instances

Diagnostics, Warnings, Errors and Error Messages

Instances

Instances

Source information (associated with constraints)

Instances

Measures

Instances

Instances

Instances

Instances

Classes describing operations on `RTypes`

Manipulating `Predicates`

Traversing `RType`