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

Which Top-Level Binders Should be Verified

Constructors

AllVars
Only ![Var]

Instances

Instances details

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

data TyConMap Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: LocSymbol -> Bool Source # isList :: LocSymbol -> Bool Source # isTuple :: LocSymbol -> Bool Source # ppTycon :: LocSymbol -> Doc Source # isClass :: LocSymbol -> Bool Source # isEqual :: LocSymbol -> Bool Source # isNumCls :: LocSymbol -> Bool Source # isFracCls :: LocSymbol -> Bool Source #
Qualify BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a Source #
REq r => REq (Located r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: Located r -> Located r -> Bool Source #
Binary (Spec LocBareType LocSymbol) Source #
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 Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: BTyCon -> BTyCon -> Bool # (/=) :: BTyCon -> BTyCon -> Bool #
Data BTyCon Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> BTyCon -> ShowS # show :: BTyCon -> String # showList :: [BTyCon] -> ShowS #
Generic BTyCon Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: BTyCon -> () #
Binary BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: BTyCon -> Put # get :: Get BTyCon # putList :: [BTyCon] -> Put #
Symbolic BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: BTyCon -> Symbol
Fixpoint BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: BTyCon -> Doc simplify :: BTyCon -> BTyCon
PPrint BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyCon -> Doc # pprintPrec :: Int -> Tidy -> BTyCon -> Doc #
Loc BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: BTyCon -> SrcSpan
Hashable BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> BTyCon -> Int hash :: BTyCon -> Int
TyConable BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: BTyCon -> Bool Source # isList :: BTyCon -> Bool Source # isTuple :: BTyCon -> Bool Source # ppTycon :: BTyCon -> Doc Source # isClass :: BTyCon -> Bool Source # isEqual :: BTyCon -> Bool Source # isNumCls :: BTyCon -> Bool Source # isFracCls :: BTyCon -> Bool Source #
Qualify BareType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType Source #
Qualify BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
FreeVar BTyCon BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: BTyCon -> [BTyVar]
SubsTy BTyVar BSort BSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort Source #
SubsTy BTyVar BSort BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #
SubsTy Symbol Symbol (BRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #
Binary (Spec LocBareType LocSymbol) Source #
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 Source #
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 Source #

isClassBTyCon :: BTyCon -> Bool Source #

newtype BTyVar Source #

Constructors

BTV Symbol

Instances

Instances details

Eq BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: BTyVar -> BTyVar -> Bool # (/=) :: BTyVar -> BTyVar -> Bool #
Data BTyVar Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> BTyVar -> ShowS # show :: BTyVar -> String # showList :: [BTyVar] -> ShowS #
IsString BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fromString :: String -> BTyVar #
Generic BTyVar Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: BTyVar -> () #
Binary BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: BTyVar -> Put # get :: Get BTyVar # putList :: [BTyVar] -> Put #
Symbolic BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: BTyVar -> Symbol
PPrint BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyVar -> Doc # pprintPrec :: Int -> Tidy -> BTyVar -> Doc #
Hashable BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> BTyVar -> Int hash :: BTyVar -> Int
Qualify BareType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType Source #
Qualify BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
FreeVar BTyCon BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: BTyCon -> [BTyVar]
SubsTy BTyVar BSort BSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort Source #
SubsTy BTyVar BSort BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #
SubsTy Symbol Symbol (BRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #
SubsTy BTyVar (RType c BTyVar ()) BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #
Binary (Spec LocBareType LocSymbol) Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep BTyVar

Refined Type Constructors

data RTyCon Source #

Constructors

RTyCon TyCon ![RPVar] !TyConInfo

Instances

Instances details

Eq RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: RTyCon -> RTyCon -> Bool # (/=) :: RTyCon -> RTyCon -> Bool #
Data RTyCon Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Show RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> RTyCon -> ShowS # show :: RTyCon -> String # showList :: [RTyCon] -> ShowS #
Generic RTyCon Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
NFData RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTyCon -> () #
Exception Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
Symbolic RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: RTyCon -> Symbol
Fixpoint RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: RTyCon -> Doc simplify :: RTyCon -> RTyCon
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint RTyCon Source #
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 Source #	TyConable Instances -------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods isFun :: RTyCon -> Bool Source # isList :: RTyCon -> Bool Source # isTuple :: RTyCon -> Bool Source # ppTycon :: RTyCon -> Doc Source # isClass :: RTyCon -> Bool Source # isEqual :: RTyCon -> Bool Source # isNumCls :: RTyCon -> Bool Source # isFracCls :: RTyCon -> Bool Source #
Result Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError Source #
Qualify SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType Source #
Qualify RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon Source #
REq SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool Source #
FreeVar RTyCon RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: RTyCon -> [RTyVar]
SubsTy tv RSort Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy TyVar Type SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy Symbol RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RSort PrType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType Source #
SubsTy RTyVar RSort RSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort Source #
SubsTy RTyVar RSort RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #
SubsTy RTyVar RTyVar SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) Source # true :: RRType r -> m (RRType r) Source # refresh :: RRType r -> m (RRType r) Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #
Exception [Error] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
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] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError Source #
Qualify (Measure SpecType DataCon) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon Source #
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 Source #
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 Source #

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

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

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

there will be:

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

Constructors

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

Instances

Instances details

Data TyConInfo Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> TyConInfo -> ShowS # show :: TyConInfo -> String # showList :: [TyConInfo] -> ShowS #
Generic TyConInfo Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: TyConInfo -> () #
Default TyConInfo Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods def :: TyConInfo
Qualify TyConInfo Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConInfo -> TyConInfo Source #
type Rep TyConInfo Source #
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 Source #

rTyConPVs :: RTyCon -> [RPVar] Source #

rTyConPropVs :: RTyCon -> [PVar RSort] Source #

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

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

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

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

Accessors for RTyCon

Refinement Types

data RType c tv r Source #

Constructors

RVar
Fields 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 Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Semigroup REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: REnv -> REnv -> REnv # sconcat :: NonEmpty REnv -> REnv # stimes :: Integral b => b -> REnv -> REnv #
Monoid REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
Exception Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
Result Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError Source #
Qualify SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType Source #
Qualify BareType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType Source #
Qualify BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
REq SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool Source #
SubsTy tv RSort Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy TyVar Type SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy Symbol RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RSort PrType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType Source #
SubsTy RTyVar RSort RSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort Source #
SubsTy RTyVar RSort RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #
SubsTy RTyVar RTyVar SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
SubsTy BTyVar BSort BSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BSort -> BSort Source #
SubsTy BTyVar BSort BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #
SubsTy Symbol Symbol (BRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> BRType r -> BRType r Source #
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) Source # true :: RRType r -> m (RRType r) Source # refresh :: RRType r -> m (RRType r) Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar Source #
SubsTy BTyVar (RType c BTyVar ()) BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #
Exception [Error] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
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] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError Source #
Functor (RType c tv) Source #
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) Source #
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) Source #
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)) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon Source #
(Eq tv, Eq r, Eq c) => Eq (RType c tv r) Source #
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 ()) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #	Pretty Printing RefType ---------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RType c tv r -> Doc # pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #
Reftable (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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RType c tv r)

data Ref τ t Source #

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

Constructors

RProp
Fields 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)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #
SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r Source #
Functor (Ref τ) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Ref τ t -> () #
(Binary τ, Binary t) => Binary (Ref τ t) Source #
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)) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: Ref t1 t2 -> Ref t1 t2 -> Bool Source #
PPrint (RTProp c tv r) => Show (RTProp c tv r) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #

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

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

newtype RTyVar Source #

Constructors

RTV TyVar

Instances

Instances details

Eq RTyVar Source #	Wrappers for GHC Type Elements --------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods (==) :: RTyVar -> RTyVar -> Bool # (/=) :: RTyVar -> RTyVar -> Bool #
Data RTyVar Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Show RTyVar Source #	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 Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
NFData RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTyVar -> () #
Exception Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
Symbolic RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: RTyVar -> Symbol
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint RTyVar Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError Source #
Qualify SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType Source #
REq SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool Source #
FreeVar RTyCon RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods freeVars :: RTyCon -> [RTyVar]
SubsTy tv RSort Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy TyVar Type SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy Symbol RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (Symbol, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort Sort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RSort PrType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType Source #
SubsTy RTyVar RSort RSort Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RSort -> RSort Source #
SubsTy RTyVar RSort RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #
SubsTy RTyVar RTyVar SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) Source # true :: RRType r -> m (RRType r) Source # refresh :: RRType r -> m (RRType r) Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #
Exception [Error] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
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] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError Source #
Qualify (Measure SpecType DataCon) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon Source #
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 Source #
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 Source #

Refinement Type Aliases

Constructors

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

Instances

Instances details

Functor (RTAlias x) Source #
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) Source #
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) Source #
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) Source #	Auxiliary Stuff Used Elsewhere ---------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods showsPrec :: Int -> RTAlias tv ty -> ShowS # show :: RTAlias tv ty -> String # showList :: [RTAlias tv ty] -> ShowS #
Generic (RTAlias x a) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #

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

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

Worlds

data HSeg t Source #

Constructors

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

Instances

Instances details

Data t => Data (HSeg t) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (HSeg t)

newtype World t Source #

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

Constructors

World [HSeg t]

Instances

Instances details

Data t => Data (World t) Source #
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) Source #
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) Source #
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 Source #

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool Source #

isList :: c -> Bool Source #

isTuple :: c -> Bool Source #

ppTycon :: c -> Doc Source #

isClass :: c -> Bool Source #

isEqual :: c -> Bool Source #

isNumCls :: c -> Bool Source #

isFracCls :: c -> Bool Source #

Instances

Instances details

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

class SubsTy tv ty a where Source #

Methods

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

Instances

Instances details

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

Type Variables

data RTVar tv s Source #

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 ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #
Eq tv => Eq (RTVar tv s) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTVar tv s -> () #
(Binary tv, Binary s) => Binary (RTVar tv s) Source #
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) Source #
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) Source #
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) Source #
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 Source #

Constructors

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

Instances

Instances details

Functor RTVInfo Source #
Instance details 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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: RTVInfo s -> () #
Binary s => Binary (RTVInfo s) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RTVInfo s -> Int hash :: RTVInfo s -> Int
type Rep (RTVInfo s) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (RTVInfo s)

makeRTVar :: tv -> RTVar tv s Source #

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

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

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

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

Predicate Variables

data PVar t Source #

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

Constructors

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

Instances

Instances details

Functor PVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> PVar a -> PVar b # (<$) :: a -> PVar b -> PVar a #
Subable UsedPVar Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> PVar ty -> PVar ty Source #
Eq (PVar t) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: PVar t -> () #
Binary t => Binary (PVar t) Source #
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) Source #	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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> PVar a -> Int hash :: PVar a -> Int
type Rep (PVar t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (PVar t)

isPropPV :: PVar t -> Bool Source #

pvType :: PVar t -> t Source #

data PVKind t Source #

Constructors

PVProp t
PVHProp

Instances

Instances details

Functor PVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> PVKind a -> PVKind b # (<$) :: a -> PVKind b -> PVKind a #
Foldable PVKind Source #
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 Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> PVKind ty -> PVKind ty Source #
Data t => Data (PVKind t) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: PVKind a -> () #
Binary a => Binary (PVKind a) Source #
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) Source #
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 Source #

Constructors

Pr [UsedPVar]

Instances

Instances details

Eq Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Predicate -> Predicate -> Bool # (/=) :: Predicate -> Predicate -> Bool #
Data Predicate Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods showsPrec :: Int -> Predicate -> ShowS # show :: Predicate -> String # showList :: [Predicate] -> ShowS #
Generic Predicate Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: Predicate # mappend :: Predicate -> Predicate -> Predicate # mconcat :: [Predicate] -> Predicate #
NFData Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Predicate -> () #
Binary Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Predicate -> Put # get :: Get Predicate # putList :: [Predicate] -> Put #
PPrint Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Predicate -> Doc # pprintPrec :: Int -> Tidy -> Predicate -> Doc #
Reftable Predicate Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Predicate -> Int hash :: Predicate -> Int
SubsTy tv RSort Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy RTyVar RSort PrType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> PrType -> PrType Source #
type Rep Predicate Source #
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 Source #

Constructors

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

Instances

Instances details

Functor UReft Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> UReft a -> UReft b # (<$) :: a -> UReft b -> UReft a #
Show Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Foldable UReft Source #
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 Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: REnv # mappend :: REnv -> REnv -> REnv # mconcat :: [REnv] -> REnv #
NFData REnv Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: REnv -> () #
Exception Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
Result Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: Error -> FixResult UserError Source #
Qualify SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType Source #
Qualify BareType Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType Source #
Qualify RReft Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft Source #
Qualify BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
REq SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: SpecType -> SpecType -> Bool Source #
Freshable m Integer => Freshable m RReft Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m RReft Source # true :: RReft -> m RReft Source # refresh :: RReft -> m RReft Source #
SubsTy TyVar Type SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy RTyVar RSort SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RTyVar SpecType Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
SubsTy tv ty r => SubsTy tv ty (UReft r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> UReft r -> UReft r Source #
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #
Eq r => Eq (UReft r) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: UReft r -> () #
Binary r => Binary (UReft r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: UReft r -> Put # get :: Get (UReft r) # putList :: [UReft r] -> Put #
Exception [Error] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
(PPrint r, Reftable r) => PPrint (UReft r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> UReft r -> Doc # pprintPrec :: Int -> Tidy -> UReft r -> Doc #
Expression (UReft ()) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods expr :: UReft () -> Expr
(PPrint r, Reftable r) => Reftable (UReft r) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> UReft r -> Int hash :: UReft r -> Int
UReftable (UReft Reft) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods ofUReft :: UReft Reft -> UReft Reft Source #
Result [Error] Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: [Error] -> FixResult UserError Source #
REq (UReft Reft) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Equality Methods (=*=) :: UReft Reft -> UReft Reft -> Bool Source #
Binary (Spec LocBareType LocSymbol) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon Source #
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) Source #
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 Source #

Termination expressions

Constructors

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

Instances

Instances details

Data SizeFun Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> SizeFun -> ShowS # show :: SizeFun -> String # showList :: [SizeFun] -> ShowS #
Generic SizeFun Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: SizeFun -> () #
Binary SizeFun Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: SizeFun -> Put # get :: Get SizeFun # putList :: [SizeFun] -> Put #
PPrint SizeFun Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> SizeFun -> Doc # pprintPrec :: Int -> Tidy -> SizeFun -> Doc #
Hashable SizeFun Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> SizeFun -> Int hash :: SizeFun -> Int
Qualify SizeFun Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun Source #
type Rep SizeFun Source #
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 Source #

data DataDecl Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataDecl -> DataDecl -> Bool # (/=) :: DataDecl -> DataDecl -> Bool #
Data DataDecl Source #
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 Source #
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 Source #	For debugging.
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataDecl -> ShowS # show :: DataDecl -> String # showList :: [DataDecl] -> ShowS #
Generic DataDecl Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataDecl -> Put # get :: Get DataDecl # putList :: [DataDecl] -> Put #
Symbolic DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: DataDecl -> Symbol
PPrint DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
Loc DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataDecl -> SrcSpan
Hashable DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataDecl -> Int hash :: DataDecl -> Int
Qualify DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl Source #
type Rep DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataDecl

data DataName Source #

The name of the TyCon corresponding to a DataDecl

Constructors

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

Instances

Instances details

Eq DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataName -> DataName -> Bool # (/=) :: DataName -> DataName -> Bool #
Data DataName Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataName -> ShowS # show :: DataName -> String # showList :: [DataName] -> ShowS #
Generic DataName Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataName -> Put # get :: Get DataName # putList :: [DataName] -> Put #
Symbolic DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: DataName -> Symbol
PPrint DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataName -> Doc # pprintPrec :: Int -> Tidy -> DataName -> Doc #
Loc DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataName -> SrcSpan
Hashable DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataName -> Int hash :: DataName -> Int
type Rep DataName Source #
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 Source #

data DataCtor Source #

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 Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataCtor -> Put # get :: Get DataCtor # putList :: [DataCtor] -> Put #
PPrint DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
Loc DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataCtor -> SrcSpan
Hashable DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataCtor -> Int hash :: DataCtor -> Int
Qualify DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor Source #
type Rep DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataCtor

data DataConP Source #

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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods showsPrec :: Int -> DataConP -> ShowS # show :: DataConP -> String # showList :: [DataConP] -> ShowS #
Generic DataConP Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> DataConP -> Doc # pprintPrec :: Int -> Tidy -> DataConP -> Doc #
Loc DataConP Source #	NOTE:DataCon-Data for each `DataConP` we also store the type of the constructed data. This is the same as `tyRes` for vanilla ADTs (e.g. List, Maybe etc.) but may differ for GADTs. For example, data Thing a where X :: Thing Int Y :: Thing Bool Here the `DataConP` associated with `X` (resp. `Y`) has `tyRes` corresponding to 'Thing Int' (resp. 'Thing Bool'), but in both cases, the `tyData` should be 'Thing a'.
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: DataConP -> SrcSpan
type Rep DataConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep DataConP

data HasDataDecl Source #

Constructors

NoDecl (Maybe SizeFun)
HasDecl

Instances

Instances details

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

hasDecl :: DataDecl -> HasDataDecl Source #

data DataDeclKind Source #

What kind of DataDecl is it?

Constructors

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

Instances

Instances details

Eq DataDeclKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: DataDeclKind -> DataDeclKind -> Bool # (/=) :: DataDeclKind -> DataDeclKind -> Bool #
Data DataDeclKind Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> DataDeclKind -> ShowS # show :: DataDeclKind -> String # showList :: [DataDeclKind] -> ShowS #
Generic DataDeclKind Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: DataDeclKind -> () #
Binary DataDeclKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: DataDeclKind -> Put # get :: Get DataDeclKind # putList :: [DataDeclKind] -> Put #
Hashable DataDeclKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> DataDeclKind -> Int hash :: DataDeclKind -> Int
type Rep DataDeclKind Source #
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 Source #

Constructors

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

Instances

Instances details

Data TyConP Source #
Instance details 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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods showsPrec :: Int -> TyConP -> ShowS # show :: TyConP -> String # showList :: [TyConP] -> ShowS #
Generic TyConP Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> TyConP -> Doc # pprintPrec :: Int -> Tidy -> TyConP -> Doc #
Loc TyConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: TyConP -> SrcSpan
Qualify TyConP Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP Source #
type Rep TyConP Source #
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 Source #

Arguments

= RType RTyCon RTyVar

Resolved version

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

type BRType Source #

Arguments

= RType BTyCon BTyVar

Bare parsed version

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

type BSort = BRType () Source #

type BPVar = PVar BSort Source #

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

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

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

Instantiated RType

type BareType = BRType RReft Source #

type PrType = RRType Predicate Source #

type SpecType = RRType RReft Source #

type SpecProp = RRProp RReft Source #

type SpecRTVar = RTVar RTyVar RSort Source #

type SpecRep = RRep RReft Source #

type LocBareType = Located BareType Source #

type LocSpecType = Located SpecType Source #

type RSort = RRType () Source #

type UsedPVar = PVar () Source #

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

type RPVar = PVar RSort Source #

type RReft = UReft Reft Source #

type REnv = AREnv SpecType Source #

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

data AREnv t Source #

Constructors

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

Instances

Instances details

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

Constructing & Destructing RTypes

data RTypeRep c tv r Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Manipulating `Predicates`

pvars :: Predicate -> [UsedPVar] Source #

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

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

Some tests on RTypes

isBase :: RType t t1 t2 -> Bool Source #

isFunTy :: RType t t1 t2 -> Bool Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

???

data Oblig Source #

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

Constructors

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

Instances

Instances details

Eq Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods (==) :: Oblig -> Oblig -> Bool # (/=) :: Oblig -> Oblig -> Bool #
Data Oblig Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods showsPrec :: Int -> Oblig -> ShowS # show :: Oblig -> String # showList :: [Oblig] -> ShowS #
Generic Oblig Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods rnf :: Oblig -> () #
Binary Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods put :: Oblig -> Put # get :: Get Oblig # putList :: [Oblig] -> Put #
PPrint Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> Oblig -> Doc # pprintPrec :: Int -> Tidy -> Oblig -> Doc #
Hashable Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods hashWithSalt :: Int -> Oblig -> Int hash :: Oblig -> Int
type Rep Oblig Source #
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 Source #

addInvCond :: SpecType -> RReft -> SpecType Source #

Inferred Annotations

newtype AnnInfo a Source #

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

Constructors

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

Instances

Instances details

Functor AnnInfo Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: AnnInfo a -> () #
PPrint a => PPrint (AnnInfo a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> AnnInfo a -> Doc # pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #
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) Source #
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 Source #

Constructors

AnnUse t
AnnDef t
AnnRDf t
AnnLoc SrcSpan

Instances

Instances details

Functor Annot Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Annot a -> () #
PPrint t => PPrint (Annot t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Annot t -> Doc # pprintPrec :: Int -> Tidy -> Annot t -> Doc #
type Rep (Annot t) Source #
Instance details 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 Source #

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

Constructors

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

Instances

Instances details

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

Overall Output

data Output a Source #

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

Constructors

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

Instances

Instances details

Functor Output Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> Output a -> Output b # (<$) :: a -> Output b -> Output a #
Generic (Output a) Source #
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) Source #
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) Source #
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) Source #
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 Source #

isHole :: Expr -> Bool Source #

hasHoleTy :: RType t t1 t2 -> Bool Source #

Converting To and From Sort

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

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

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

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

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

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

Class for values that can be pretty printed

class PPrint a where #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> SourceError -> Doc # pprintPrec :: Int -> Tidy -> SourceError -> Doc #
PPrint AltCon Source #
Instance details Defined in Language.Haskell.Liquid.Synthesize.Misc Methods pprintTidy :: Tidy -> AltCon -> Doc # pprintPrec :: Int -> Tidy -> AltCon -> Doc #
PPrint Class Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Class -> Doc # pprintPrec :: Int -> Tidy -> Class -> Doc #
PPrint DataCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #
PPrint Type Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Type -> Doc # pprintPrec :: Int -> Tidy -> Type -> Doc #
PPrint TyThing Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> TyThing -> Doc # pprintPrec :: Int -> Tidy -> TyThing -> Doc #
PPrint Var Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Var -> Doc # pprintPrec :: Int -> Tidy -> Var -> Doc #
PPrint ErrMsg Source #	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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> SrcSpan -> Doc # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #
PPrint TyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> TyCon -> Doc # pprintPrec :: Int -> Tidy -> TyCon -> Doc #
PPrint Name Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Name -> Doc # pprintPrec :: Int -> Tidy -> Name -> Doc #
PPrint ParseError Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Tidy -> Doc # pprintPrec :: Int -> Tidy -> Tidy -> Doc #
PPrint Bop
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Bop -> Doc # pprintPrec :: Int -> Tidy -> Bop -> Doc #
PPrint Brel
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc # pprintPrec :: Int -> Tidy -> Brel -> Doc #
PPrint Constant
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc # pprintPrec :: Int -> Tidy -> Constant -> Doc #
PPrint 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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> UserError -> Doc # pprintPrec :: Int -> Tidy -> UserError -> Doc #
PPrint Oblig Source #
Instance details Defined in Language.Haskell.Liquid.Types.Errors Methods pprintTidy :: Tidy -> Oblig -> Doc # pprintPrec :: Int -> Tidy -> Oblig -> Doc #
PPrint KVProf Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVProf -> Doc # pprintPrec :: Int -> Tidy -> KVProf -> Doc #
PPrint KVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVKind -> Doc # pprintPrec :: Int -> Tidy -> KVKind -> Doc #
PPrint Body Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Body -> Doc # pprintPrec :: Int -> Tidy -> Body -> Doc #
PPrint ModName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> ModName -> Doc # pprintPrec :: Int -> Tidy -> ModName -> Doc #
PPrint Error Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> Error -> Doc # pprintPrec :: Int -> Tidy -> Error -> Doc #
PPrint HasDataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc #
PPrint SizeFun Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> SizeFun -> Doc # pprintPrec :: Int -> Tidy -> SizeFun -> Doc #
PPrint DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
PPrint DataName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> DataName -> Doc # pprintPrec :: Int -> Tidy -> DataName -> Doc #
PPrint DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Types.RefType Methods pprintTidy :: Tidy -> DataDecl -> Doc # pprintPrec :: Int -> Tidy -> DataDecl -> Doc #
PPrint RTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyCon -> Doc # pprintPrec :: Int -> Tidy -> RTyCon -> Doc #
PPrint BTyCon Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyCon -> Doc # pprintPrec :: Int -> Tidy -> BTyCon -> Doc #
PPrint RTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RTyVar -> Doc # pprintPrec :: Int -> Tidy -> RTyVar -> Doc #
PPrint BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> BTyVar -> Doc # pprintPrec :: Int -> Tidy -> BTyVar -> Doc #
PPrint Predicate Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Predicate -> Doc # pprintPrec :: Int -> Tidy -> Predicate -> Doc #
PPrint TargetVars Source #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetVars -> Doc # pprintPrec :: Int -> Tidy -> TargetVars -> Doc #
PPrint DataConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> DataConP -> Doc # pprintPrec :: Int -> Tidy -> DataConP -> Doc #
PPrint TyConP Source #
Instance details Defined in Language.Haskell.Liquid.Types.PredType Methods pprintTidy :: Tidy -> TyConP -> Doc # pprintPrec :: Int -> Tidy -> TyConP -> Doc #
PPrint LMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LMap -> Doc # pprintPrec :: Int -> Tidy -> LMap -> Doc #
PPrint LogicMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> LogicMap -> Doc # pprintPrec :: Int -> Tidy -> LogicMap -> Doc #
PPrint Pattern Source #
Instance details Defined in Language.Haskell.Liquid.GHC.Resugar Methods pprintTidy :: Tidy -> Pattern -> Doc # pprintPrec :: Int -> Tidy -> Pattern -> Doc #
PPrint TargetSpec Source #	Pretty Printing -----------------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetSpec -> Doc # pprintPrec :: Int -> Tidy -> TargetSpec -> Doc #
PPrint TargetInfo Source #
Instance details Defined in Language.Haskell.Liquid.GHC.Interface Methods pprintTidy :: Tidy -> TargetInfo -> Doc # pprintPrec :: Int -> Tidy -> TargetInfo -> Doc #
PPrint DiffCheck Source #
Instance details Defined in Language.Haskell.Liquid.UX.DiffCheck Methods pprintTidy :: Tidy -> DiffCheck -> Doc # pprintPrec :: Int -> Tidy -> DiffCheck -> Doc #
PPrint CGInfo Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> CGInfo -> Doc # pprintPrec :: Int -> Tidy -> CGInfo -> Doc #
PPrint WfC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> WfC -> Doc # pprintPrec :: Int -> Tidy -> WfC -> Doc #
PPrint SubC Source #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods pprintTidy :: Tidy -> SubC -> Doc # pprintPrec :: Int -> Tidy -> SubC -> Doc #
PPrint CGEnv Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Expr Var -> Doc # pprintPrec :: Int -> Tidy -> Expr Var -> Doc #
PPrint (Bind Var) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Bind Var -> Doc # pprintPrec :: Int -> Tidy -> Bind Var -> Doc #
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) Source #	Pretty Printing Error Messages -------------------------------------------- Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError Doc -> Doc # pprintPrec :: Int -> Tidy -> CtxError Doc -> Doc #
PPrint (CtxError SpecType) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods pprintTidy :: Tidy -> CtxError SpecType -> Doc # pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #
PPrint t => PPrint (Annot t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> Annot t -> Doc # pprintPrec :: Int -> Tidy -> Annot t -> Doc #
PPrint a => PPrint (AnnInfo a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> AnnInfo a -> Doc # pprintPrec :: Int -> Tidy -> AnnInfo a -> Doc #
PPrint t => PPrint (RClass t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RClass t -> Doc # pprintPrec :: Int -> Tidy -> RClass t -> Doc #
PPrint t => PPrint (CMeasure t) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> RISig t -> Doc # pprintPrec :: Int -> Tidy -> RISig t -> Doc #
PPrint t => PPrint (RILaws t) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> UReft r -> Doc # pprintPrec :: Int -> Tidy -> UReft r -> Doc #
PPrint (PVar a) Source #	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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods pprintTidy :: Tidy -> PlugTV v -> Doc # pprintPrec :: Int -> Tidy -> PlugTV v -> Doc #
(PPrint a, PPrint 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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MSpec t a -> Doc # pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #
PPrint t => PPrint (HoleInfo i t) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HoleInfo i t -> Doc # pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc #
(PPrint t, PPrint a) => PPrint (Measure t a) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc #
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #	Pretty Printing RefType ---------------------------------------------------
Instance details Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RType c tv r -> Doc # pprintPrec :: Int -> Tidy -> RType c tv r -> Doc #
(PPrint a, PPrint 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 Source #

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

Constructors

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

Instances

Instances details

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

ppEnv :: PPEnv Source #

ppEnvShort :: PPEnv -> PPEnv Source #

Modules and Imports

data ModName Source #

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

Constructors

ModName !ModType !ModuleName

Instances

Instances details

Eq ModName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: ModName -> ModName -> Bool # (/=) :: ModName -> ModName -> Bool #
Data ModName Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> ModName -> ShowS # show :: ModName -> String # showList :: [ModName] -> ShowS #
Generic ModName Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods symbol :: ModName -> Symbol
PPrint ModName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> ModName -> Doc # pprintPrec :: Int -> Tidy -> ModName -> Doc #
Hashable ModName Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> ModName -> Int hash :: ModName -> Int
Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
type Rep ModName Source #
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 Source #

Constructors

Target
SrcImport
SpecImport

Instances

Instances details

Eq ModType Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: ModType -> ModType -> Bool # (/=) :: ModType -> ModType -> Bool #
Data ModType Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> ModType -> ShowS # show :: ModType -> String # showList :: [ModType] -> ShowS #
Generic ModType Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> ModType -> Int hash :: ModType -> Int
type Rep ModType Source #
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 Source #

isSpecImport :: ModName -> Bool Source #

isTarget :: ModName -> Bool Source #

getModName :: ModName -> ModuleName Source #

getModString :: ModName -> String Source #

qualifyModName :: ModName -> Symbol -> Symbol Source #

Refinement Type Aliases

data RTEnv tv t Source #

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

Constructors

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

Instances

Instances details

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

type BareRTEnv = RTEnv Symbol BareType Source #

type SpecRTEnv = RTEnv RTyVar SpecType Source #

type BareRTAlias = RTAlias Symbol BareType Source #

type SpecRTAlias = RTAlias RTyVar SpecType Source #

Diagnostics, Warnings, Errors and Error Messages

module Language.Haskell.Liquid.Types.Errors

type Error = TError SpecType Source #

type ErrorResult = FixResult UserError Source #

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

data Warning Source #

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

Instances

Instances details

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

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

data Diagnostics Source #

Instances

Instances details

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

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

emptyDiagnostics :: Diagnostics Source #

noErrors :: Diagnostics -> Bool Source #

allWarnings :: Diagnostics -> [Warning] Source #

allErrors :: Diagnostics -> [Error] Source #

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

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

Source information (associated with constraints)

data Cinfo Source #

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

Constructors

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

Instances

Instances details

Eq Cinfo Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Cinfo -> Cinfo -> Bool # (/=) :: Cinfo -> Cinfo -> Bool #
Ord Cinfo Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Cinfo -> ShowS # show :: Cinfo -> String # showList :: [Cinfo] -> ShowS #
Generic Cinfo Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: Cinfo -> () #
Fixpoint Cinfo Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods toFix :: Cinfo -> Doc simplify :: Cinfo -> Cinfo
Loc Cinfo Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: Cinfo -> SrcSpan
Result (FixResult Cinfo) Source #
Instance details Defined in Language.Haskell.Liquid.UX.Tidy Methods result :: FixResult Cinfo -> FixResult UserError Source #
type Rep Cinfo Source #
Instance details 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 Source #

Constructors

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

Instances

Instances details

Bifunctor Measure Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source #
Functor (Measure ty) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods srcSpan :: Measure a b -> SrcSpan
(Hashable ty, Hashable ctor) => Hashable (Measure ty ctor) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon Source #
type Rep (Measure ty ctor) Source #
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] Source #

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

data MeasureKind Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: MeasureKind -> MeasureKind -> Bool # (/=) :: MeasureKind -> MeasureKind -> Bool #
Data MeasureKind Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MeasureKind -> ShowS # show :: MeasureKind -> String # showList :: [MeasureKind] -> ShowS #
Generic MeasureKind Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: MeasureKind -> Put # get :: Get MeasureKind # putList :: [MeasureKind] -> Put #
Hashable MeasureKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> MeasureKind -> Int hash :: MeasureKind -> Int
type Rep MeasureKind Source #
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 Source #

Constructors

CM
Fields cName :: LocSymbol cSort :: ty

Instances

Instances details

Functor CMeasure Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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 Source #

Constructors

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

Instances

Instances details

Bifunctor Def Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor Source #
type Rep (Def ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (Def ty ctor)

data Body Source #

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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: Body -> Body -> Bool # (/=) :: Body -> Body -> Bool #
Data Body Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> Body -> ShowS # show :: Body -> String # showList :: [Body] -> ShowS #
Generic Body Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods put :: Body -> Put # get :: Get Body # putList :: [Body] -> Put #
PPrint Body Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> Body -> Doc # pprintPrec :: Int -> Tidy -> Body -> Doc #
Subable Body Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> Body -> Int hash :: Body -> Int
Qualify Body Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body Source #
type Rep Body Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep Body

data MSpec ty ctor Source #

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 Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (MSpec ty ctor)

Scoping Info

type BScope = Bool Source #

Information about scope Binders Scope in

Type Classes

data RClass ty Source #

Constructors

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

Instances

Instances details

Functor RClass Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RClass ty -> Int hash :: RClass ty -> Int
type Rep (RClass ty) Source #
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 Source #

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

Constructors

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

Instances

Instances details

Eq KVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (==) :: KVKind -> KVKind -> Bool # (/=) :: KVKind -> KVKind -> Bool #
Data KVKind Source #
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 Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> KVKind -> ShowS # show :: KVKind -> String # showList :: [KVKind] -> ShowS #
Generic KVKind Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: KVKind -> () #
PPrint KVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVKind -> Doc # pprintPrec :: Int -> Tidy -> KVKind -> Doc #
Hashable KVKind Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> KVKind -> Int hash :: KVKind -> Int
type Rep KVKind Source #
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 Source #

Instances

Instances details

Generic KVProf Source #
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 Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods rnf :: KVProf -> () #
PPrint KVProf Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> KVProf -> Doc # pprintPrec :: Int -> Tidy -> KVProf -> Doc #
type Rep KVProf Source #
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 Source #

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

Misc

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

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

CoreToLogic

data LogicMap Source #

Constructors

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

Instances

Instances details

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

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

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

data LMap Source #

Constructors

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

Instances

Instances details

Show LMap Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> LMap -> ShowS # show :: LMap -> String # showList :: [LMap] -> ShowS #
PPrint LMap Source #
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 Source #

newtype DEnv x ty Source #

Constructors

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

Instances

Instances details

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

data RInstance t Source #

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

Constructors

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

Instances

Instances details

Functor RInstance Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RInstance t -> Int hash :: RInstance t -> Int
type Rep (RInstance t) Source #
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 Source #

Constructors

RIAssumed t
RISig t

Instances

Instances details

Functor RISig Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RISig t -> Int hash :: RISig t -> Int
type Rep (RISig t) Source #
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 Source #

Constructors

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

Instances

Instances details

Functor RILaws Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods hashWithSalt :: Int -> RILaws ty -> Int hash :: RILaws ty -> Int
type Rep (RILaws ty) Source #
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 Source #

Constructors

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

Instances

Instances details

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

Ureftable Instances

class Reftable r => UReftable r where Source #

Minimal complete definition

Nothing

Methods

ofUReft :: UReft Reft -> r Source #

Instances

Instances details

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

String Literals

liquidBegin :: String Source #

liquidEnd :: String Source #

data Axiom b s e Source #

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

rtyVarType :: RTyVar -> Type Source #

tyVarVar :: RTVar RTyVar c -> Var Source #

Orphan instances

Ord DataCon Source #
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 Source #
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 Source #
Instance details Methods showsPrec :: Int -> DataCon -> ShowS # show :: DataCon -> String # showList :: [DataCon] -> ShowS #
Show ModuleName Source #
Instance details Methods showsPrec :: Int -> ModuleName -> ShowS # show :: ModuleName -> String # showList :: [ModuleName] -> ShowS #
Symbolic DataCon Source #
Instance details Methods symbol :: DataCon -> Symbol
Symbolic ModuleName Source #
Instance details Methods symbol :: ModuleName -> Symbol
PPrint DataCon Source #
Instance details Methods pprintTidy :: Tidy -> DataCon -> Doc # pprintPrec :: Int -> Tidy -> DataCon -> Doc #
PPrint TyThing Source #
Instance details Methods pprintTidy :: Tidy -> TyThing -> Doc # pprintPrec :: Int -> Tidy -> TyThing -> Doc #
Hashable ModuleName Source #
Instance details Methods hashWithSalt :: Int -> ModuleName -> Int hash :: ModuleName -> Int
NFData a => NFData (TError a) Source #
Instance details Methods rnf :: TError a -> () #
Subable t => Subable (WithModel t) Source #
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`