Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell98 |
- 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
- Relational predicates
- 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
- Refined Function Info
- Orphan instances
This module should contain all the global type definitions and basic instances.
Synopsis
- module Language.Haskell.Liquid.UX.Config
- data TargetVars
- data TyConMap = TyConMap {}
- data Located a = Loc {}
- dummyLoc :: a -> Located a
- type LocSymbol = Located Symbol
- type LocText = Located Text
- dummyName :: Symbol
- isDummy :: Symbolic a => a -> Bool
- data BTyCon = BTyCon {}
- mkBTyCon :: LocSymbol -> BTyCon
- isClassBTyCon :: BTyCon -> Bool
- newtype BTyVar = BTV Symbol
- data RTyCon = RTyCon TyCon ![RPVar] !TyConInfo
- data TyConInfo = TyConInfo {}
- 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
- isEmbeddedClass :: TyConable c => RType c t t1 -> Bool
- data RType c tv r
- data Ref τ t = RProp {}
- 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 {}
- 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)
- data HSeg t
- newtype World t = World [HSeg t]
- class Eq c => TyConable c where
- 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
- = RTVNoInfo {
- 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 {}
- isPropPV :: PVar t -> Bool
- pvType :: PVar t -> t
- data PVKind t
- newtype Predicate = Pr [UsedPVar]
- data UReft r = MkUReft {}
- data RelExpr
- data SizeFun
- szFun :: SizeFun -> Symbol -> Expr
- data DataDecl = DataDecl {}
- data DataName
- dataNameSymbol :: DataName -> LocSymbol
- data DataCtor = DataCtor {}
- data DataConP = DataConP {}
- data HasDataDecl
- hasDecl :: DataDecl -> HasDataDecl
- data DataDeclKind
- 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 {}
- data RTypeRep c tv r = RTypeRep {}
- 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, RFInfo, RType c tv r, r)] -> RType c tv r -> RType c tv r
- bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
- bkArrow :: RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
- safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [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)
- bkUnivClass' :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType)
- rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
- rFun' :: Monoid r => RFInfo -> 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
- rFunDebug :: Monoid r => Symbol -> RType c tv r -> 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
- mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
- foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
- data Oblig
- 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
- data HoleInfo i t = HoleInfo {}
- data Output a = O {}
- 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 {}
- ppEnv :: PPEnv
- ppEnvShort :: PPEnv -> PPEnv
- data ModName = ModName !ModType !ModuleName
- data ModType
- 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 :: Logger -> DynFlags -> Warning -> IO ()
- data Cinfo = Ci {}
- 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
- data CMeasure ty = CM {}
- data Def ty ctor = Def {}
- data Body
- data MSpec ty ctor = MSpec {}
- type BScope = Bool
- data RClass ty = RClass {}
- data KVKind
- 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 {}
- toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap
- eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr
- data LMap = LMap {}
- type RDEnv = DEnv Var SpecType
- newtype DEnv x ty = DEnv (HashMap x (HashMap Symbol (RISig ty)))
- data RInstance t = RI {}
- data RISig t
- data RILaws ty = RIL {}
- data MethodType t = MT {
- tyInstance :: !(Maybe t)
- tyClass :: !(Maybe t)
- getMethodType :: MethodType t -> Maybe t
- class Reftable r => UReftable r where
- liquidBegin :: String
- liquidEnd :: String
- data Axiom b s e = Axiom {}
- type HAxiom = Axiom Var Type CoreExpr
- rtyVarType :: RTyVar -> Type
- tyVarVar :: RTVar RTyVar c -> Var
- newtype RFInfo = RFInfo {}
- defRFInfo :: RFInfo
- mkRFInfo :: Config -> RFInfo
- classRFInfo :: Bool -> RFInfo
- classRFInfoType :: Bool -> RType c tv r -> RType c tv r
- ordSrcSpan :: SrcSpan -> SrcSpan -> Ordering
Options
Ghc Information
data TargetVars Source #
Which Top-Level Binders Should be Verified
Instances
PPrint TargetVars Source # | |
Defined in Language.Haskell.Liquid.GHC.Interface pprintTidy :: Tidy -> TargetVars -> Doc # pprintPrec :: Int -> Tidy -> TargetVars -> Doc # |
Information about Type Constructors
F.Located Things
Instances
Symbols
type LocSymbol = Located Symbol #
Located Symbols -----------------------------------------------------
Default unknown name
Bare Type Constructors and Variables
Instances
isClassBTyCon :: BTyCon -> Bool Source #
BTV Symbol |
Instances
Refined Type Constructors
Instances
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]
TyConInfo | |
|
Instances
Data TyConInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConInfo -> c TyConInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConInfo # toConstr :: TyConInfo -> Constr # dataTypeOf :: TyConInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConInfo) # gmapT :: (forall b. Data b => b -> b) -> TyConInfo -> TyConInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> TyConInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConInfo -> m TyConInfo # | |
Generic TyConInfo Source # | |
Show TyConInfo Source # | |
Default TyConInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
NFData TyConInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Qualify TyConInfo Source # | |
type Rep TyConInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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))))) |
Refinement Types
RVar | |
RFun | |
RAllT | |
RAllP | "forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ (rt_pvbind) |
RApp | For example, in [a]- v > h}>, we apply (via |
RAllE | |
REx | |
RExprArg (Located Expr) | For expression arguments to type aliases see testsposvector2.hs |
RAppTy | |
RRTy | |
RHole r | let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs |
Instances
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.
Instances
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.
Instances
Refinement Type Aliases
Instances
Functor (RTAlias x) Source # | |
(Data x, Data a) => Data (RTAlias x a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTAlias x a -> c (RTAlias x a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTAlias x a) # toConstr :: RTAlias x a -> Constr # dataTypeOf :: RTAlias x a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTAlias x a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTAlias x a)) # gmapT :: (forall b. Data b => b -> b) -> RTAlias x a -> RTAlias x a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQ :: (forall d. Data d => d -> u) -> RTAlias x a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTAlias x a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # | |
Generic (RTAlias x a) Source # | |
(Show tv, Show ty) => Show (RTAlias tv ty) Source # | Auxiliary Stuff Used Elsewhere --------------------------------------------- |
(Binary x, Binary a) => Binary (RTAlias x a) Source # | |
(Eq x, Eq a) => Eq (RTAlias x a) Source # | |
(Hashable x, Hashable a) => Hashable (RTAlias x a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
(PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
Qualify a => Qualify (RTAlias Symbol a) Source # | |
type Rep (RTAlias x a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
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 #
Worlds
Instances
Data t => Data (HSeg t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
type Rep (HSeg t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
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.
Instances
Data t => Data (World t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
type Rep (World t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Classes describing operations on RTypes
class Eq c => TyConable c where Source #
Instances
class SubsTy tv ty a where Source #
Instances
Type Variables
RTVar | |
|
Instances
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # | |
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # | |
(Data tv, Data s) => Data (RTVar tv s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVar tv s -> c (RTVar tv s) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVar tv s) # toConstr :: RTVar tv s -> Constr # dataTypeOf :: RTVar tv s -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVar tv s)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVar tv s)) # gmapT :: (forall b. Data b => b -> b) -> RTVar tv s -> RTVar tv s # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVar tv s -> r # gmapQ :: (forall d. Data d => d -> u) -> RTVar tv s -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVar tv s -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVar tv s -> m (RTVar tv s) # | |
Generic (RTVar tv s) Source # | |
Show tv => Show (RTVU c tv) Source # | |
(Binary tv, Binary s) => Binary (RTVar tv s) Source # | |
(NFData tv, NFData s) => NFData (RTVar tv s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq tv => Eq (RTVar tv s) Source # | |
(Hashable tv, Hashable s) => Hashable (RTVar tv s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint v => PPrint (RTVar v s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RTVar tv s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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)))) |
RTVNoInfo | |
| |
RTVInfo | |
|
Instances
Functor RTVInfo Source # | |
Data s => Data (RTVInfo s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
Binary s => Binary (RTVInfo s) Source # | |
NFData s => NFData (RTVInfo s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq s => Eq (RTVInfo s) Source # | |
Hashable s => Hashable (RTVInfo s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RTVInfo s) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s Source #
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 Source #
Predicate Variables
Abstract Predicate Variables ----------------------------------
Instances
Functor PVar Source # | |
Subable UsedPVar Source # | |
SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source # | |
Data t => Data (PVar t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Generic (PVar t) Source # | |
Show t => Show (PVar t) Source # | |
Binary t => Binary (PVar t) Source # | |
NFData t => NFData (PVar t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq (PVar t) Source # | |
Ord (PVar t) Source # | |
Hashable (PVar a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint (PVar a) Source # | F.PPrint ----------------------------------------------------------------- |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (PVar t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Instances
Foldable PVKind Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # elem :: Eq a => a -> PVKind a -> Bool # maximum :: Ord a => PVKind a -> a # minimum :: Ord a => PVKind a -> a # | |
Traversable PVKind Source # | |
Functor PVKind Source # | |
SubsTy tv ty ty => SubsTy tv ty (PVKind ty) Source # | |
Data t => Data (PVKind t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Generic (PVKind t) Source # | |
Show t => Show (PVKind t) Source # | |
Binary a => Binary (PVKind a) Source # | |
NFData a => NFData (PVKind a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (PVKind t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (PVKind t) = D1 ('MetaData "PVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "PVProp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "PVHProp" 'PrefixI 'False) (U1 :: Type -> Type)) |
Instances
Refinements
Instances
Relational predicates
Instances
Data RelExpr Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelExpr -> c RelExpr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RelExpr # toConstr :: RelExpr -> Constr # dataTypeOf :: RelExpr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RelExpr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelExpr) # gmapT :: (forall b. Data b => b -> b) -> RelExpr -> RelExpr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelExpr -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelExpr -> r # gmapQ :: (forall d. Data d => d -> u) -> RelExpr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RelExpr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExpr -> m RelExpr # | |
Generic RelExpr Source # | |
Show RelExpr Source # | |
Binary RelExpr Source # | |
Eq RelExpr Source # | |
PPrint RelExpr Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep RelExpr Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Parse-time entities describing refined data types
Termination expressions
IdSizeFun | x -> F.EVar x |
SymSizeFun LocSymbol | x -> f x |
Instances
Data SizeFun Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
Generic SizeFun Source # | |
Show SizeFun Source # | |
Binary SizeFun Source # | |
NFData SizeFun Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq SizeFun Source # | |
Hashable SizeFun Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint SizeFun Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Qualify SizeFun Source # | |
type Rep SizeFun Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep SizeFun = D1 ('MetaData "SizeFun" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "IdSizeFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SymSizeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol))) |
Data type refinements
DataDecl | |
|
Instances
Instances
dataNameSymbol :: DataName -> LocSymbol Source #
Data Constructor
Instances
Data DataCtor Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
Binary DataCtor Source # | |
Eq DataCtor Source # | |
Hashable DataCtor Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint DataCtor Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
Loc DataCtor Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Qualify DataCtor Source # | |
type Rep DataCtor Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
DataConP | |
|
Instances
Data DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
Generic DataConP Source # | |
Show DataConP Source # | |
PPrint DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.PredType | |
Loc DataConP Source # |
Here the |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
data HasDataDecl Source #
Instances
Show HasDataDecl Source # | |
Defined in Language.Haskell.Liquid.Types.Types showsPrec :: Int -> HasDataDecl -> ShowS # show :: HasDataDecl -> String # showList :: [HasDataDecl] -> ShowS # | |
PPrint HasDataDecl Source # | |
Defined in Language.Haskell.Liquid.Types.Types pprintTidy :: Tidy -> HasDataDecl -> Doc # pprintPrec :: Int -> Tidy -> HasDataDecl -> Doc # |
hasDecl :: DataDecl -> HasDataDecl Source #
data DataDeclKind Source #
What kind of DataDecl
is it?
DataUser | User defined data-definitions (should have refined fields) |
DataReflected | Automatically lifted data-definitions (do not have refined fields) |
Instances
TyConP | |
|
Instances
Pre-instantiated RType
type RTVU c tv = RTVar tv (RType c tv ()) Source #
Unified Representation of Refinement Types --------------------------------
Instantiated RType
type LocBareType = Located BareType Source #
type LocSpecType = Located SpecType Source #
type UsedPVar = PVar () Source #
Predicates ----------------------------------------------------------------
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
Constructing & Destructing RTypes
Constructor and Destructors for RTypes ------------------------------------
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, RFInfo, RType c tv r, r)] -> RType c tv r -> RType c tv r Source #
safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [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 #
bkUnivClass' :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType) Source #
Manipulating Predicates
Some tests on RTypes
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 #
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 ------------------------------------------------------------------
???
Different kinds of Check Obligations ------------------------------------
OTerm | Obligation that proves termination |
OInv | Obligation that proves invariants |
OCons | Obligation that proves subtyping constraints |
Instances
Data Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors 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 # dataTypeOf :: Oblig -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Oblig) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig) # gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Oblig -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # | |
Generic Oblig Source # | |
Show Oblig Source # | |
Binary Oblig Source # | |
NFData Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
Eq Oblig Source # | |
Hashable Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
PPrint Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
type Rep Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type))) |
ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source #
Inferred Annotations
Annotations -------------------------------------------------------
Instances
Functor AnnInfo Source # | |
FromJSON a => FromJSON (AnnInfo a) Source # | |
ToJSON a => ToJSON (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.UX.DiffCheck | |
Data a => Data (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Monoid (AnnInfo a) Source # | |
Semigroup (AnnInfo a) Source # | |
Generic (AnnInfo a) Source # | |
PPrint a => Show (AnnInfo a) Source # | |
NFData a => NFData (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint a => PPrint (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
type Rep (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (AnnInfo a) = D1 ('MetaData "AnnInfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "AI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SrcSpan [(Maybe Text, a)])))) |
Instances
Functor Annot Source # | |
Data t => Data (Annot t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # | |
NFData a => NFData (Annot a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint t => PPrint (Annot t) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
type Rep (Annot t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (Annot t) = D1 ('MetaData "Annot" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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
Var Hole Info -----------------------------------------------------
Overall Output
Output --------------------------------------------------------------------
Instances
Refinement Hole
Converting To and From Sort
rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source #
stripRTypeBase :: RType c tv r -> Maybe r Source #
Class for values that can be pretty printed
Implement either pprintTidy
or pprintPrec
Nothing
pprintTidy :: Tidy -> a -> Doc #
pprintPrec :: Int -> Tidy -> a -> Doc #
Instances
Printer Configuration
Printer ----------------------------------------------------------------
ppEnvShort :: PPEnv -> PPEnv Source #
Modules and Imports
Module Names --------------------------------------------------------------
Instances
Instances
Data ModType Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModType -> c ModType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModType # toConstr :: ModType -> Constr # dataTypeOf :: ModType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModType) # gmapT :: (forall b. Data b => b -> b) -> ModType -> ModType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQ :: (forall d. Data d => d -> u) -> ModType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # | |
Generic ModType Source # | |
Show ModType Source # | |
Eq ModType Source # | |
Ord ModType Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Hashable ModType Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep ModType Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 #
getModName :: ModName -> ModuleName Source #
getModString :: ModName -> String Source #
qualifyModName :: ModName -> Symbol -> Symbol Source #
Refinement Type Aliases
Refinement Type Aliases ---------------------------------------------------
RTE | |
|
type BareRTAlias = RTAlias Symbol BareType Source #
Diagnostics, Warnings, Errors and Error Messages
type ErrorResult = FixResult UserError Source #
Error Data Type -----------------------------------------------------------
Diagnostic info -----------------------------------------------------------
data Diagnostics Source #
Instances
Monoid Diagnostics Source # | |
Defined in Language.Haskell.Liquid.Types.Types mempty :: Diagnostics # mappend :: Diagnostics -> Diagnostics -> Diagnostics # mconcat :: [Diagnostics] -> Diagnostics # | |
Semigroup Diagnostics Source # | |
Defined in Language.Haskell.Liquid.Types.Types (<>) :: Diagnostics -> Diagnostics -> Diagnostics # sconcat :: NonEmpty Diagnostics -> Diagnostics # stimes :: Integral b => b -> Diagnostics -> Diagnostics # | |
Eq Diagnostics Source # | |
Defined in Language.Haskell.Liquid.Types.Types (==) :: Diagnostics -> Diagnostics -> Bool # (/=) :: Diagnostics -> Diagnostics -> Bool # |
mkDiagnostics :: [Warning] -> [Error] -> Diagnostics Source #
noErrors :: Diagnostics -> Bool Source #
allWarnings :: Diagnostics -> [Warning] Source #
allErrors :: Diagnostics -> [Error] Source #
printWarning :: Logger -> DynFlags -> Warning -> IO () Source #
Printing Warnings ---------------------------------------------------------
Source information (associated with constraints)
Source Information Associated With Constraints ----------------------------
Instances
Generic Cinfo Source # | |
Show Cinfo Source # | |
NFData Cinfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq Cinfo Source # | |
Fixpoint Cinfo Source # | |
PPrint Cinfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Loc Cinfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Result (FixResult Cinfo) Source # | |
type Rep Cinfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep Cinfo = D1 ('MetaData "Cinfo" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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
M | |
|
Instances
Bifunctor Measure Source # | |
Qualify BareMeasure Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source # | |
Functor (Measure ty) Source # | |
(Data ty, Data ctor) => Data (Measure ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Generic (Measure ty ctor) Source # | |
PPrint (Measure t a) => Show (Measure t a) Source # | |
(Binary t, Binary c) => Binary (Measure t c) Source # | |
(Eq ty, Eq ctor) => Eq (Measure ty ctor) Source # | |
(Hashable ty, Hashable ctor) => Hashable (Measure ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
(PPrint t, PPrint a) => PPrint (Measure t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Subable (Measure ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Loc (Measure a b) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Qualify (Measure SpecType DataCon) Source # | |
type Rep (Measure ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (Measure ty ctor) = D1 ('MetaData "Measure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 #
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
Functor CMeasure Source # | |
Data ty => Data (CMeasure ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMeasure ty -> c (CMeasure ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CMeasure ty) # toConstr :: CMeasure ty -> Constr # dataTypeOf :: CMeasure ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CMeasure ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CMeasure ty)) # gmapT :: (forall b. Data b => b -> b) -> CMeasure ty -> CMeasure ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQ :: (forall d. Data d => d -> u) -> CMeasure ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CMeasure ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # | |
Generic (CMeasure ty) Source # | |
PPrint (CMeasure t) => Show (CMeasure t) Source # | |
PPrint t => PPrint (CMeasure t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (CMeasure ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty))) |
Instances
Bifunctor Def Source # | |
Functor (Def ty) Source # | |
(Data ty, Data ctor) => Data (Def ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Generic (Def ty ctor) Source # | |
(Show ctor, Show ty) => Show (Def ty ctor) Source # | |
(Binary t, Binary c) => Binary (Def t c) Source # | |
(Eq ctor, Eq ty) => Eq (Def ty ctor) Source # | |
(Hashable ctor, Hashable ty) => Hashable (Def ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint a => PPrint (Def t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Subable (Def ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Qualify (Def ty ctor) Source # | |
type Rep (Def ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Measures
E Expr | Measure Refinement: {v | v = e } |
P Expr | Measure Refinement: {v | (? v) = p } |
R Symbol Expr | Measure Refinement: {v | p} |
Instances
Data Body Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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 # 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 # | |
Generic Body Source # | |
Show Body Source # | |
Binary Body Source # | |
Eq Body Source # | |
Hashable Body Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint Body Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Subable Body Source # | |
Qualify Body Source # | |
type Rep Body Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Instances
Bifunctor MSpec Source # | |
Functor (MSpec ty) Source # | |
(Data ty, Data ctor) => Data (MSpec ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Eq ctor => Monoid (MSpec ty ctor) Source # | |
Eq ctor => Semigroup (MSpec ty ctor) Source # | |
Generic (MSpec ty ctor) Source # | |
(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source # | |
(PPrint t, PPrint a) => PPrint (MSpec t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (MSpec ty ctor) Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
Scoping Info
Type Classes
Instances
Functor RClass Source # | |
Data ty => Data (RClass ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RClass ty -> c (RClass ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RClass ty) # toConstr :: RClass ty -> Constr # dataTypeOf :: RClass ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RClass ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RClass ty)) # gmapT :: (forall b. Data b => b -> b) -> RClass ty -> RClass ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQ :: (forall d. Data d => d -> u) -> RClass ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RClass ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # | |
Generic (RClass ty) Source # | |
Show ty => Show (RClass ty) Source # | |
Binary ty => Binary (RClass ty) Source # | |
Eq ty => Eq (RClass ty) Source # | |
Hashable ty => Hashable (RClass ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint t => PPrint (RClass t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RClass ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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
KVar Profile --------------------------------------------------------------
RecBindE Var | Recursive binder |
NonRecBindE Var | Non recursive binder |
TypeInstE | |
PredInstE | |
LamE | |
CaseE Int | Int is the number of cases |
LetE | |
ProjectE | Projecting out field of |
Instances
Instances
Generic KVProf Source # | |
NFData KVProf Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint KVProf Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep KVProf Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep KVProf = D1 ('MetaData "KVProf" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "KVP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap KVKind Int)))) |
emptyKVProf :: KVProf Source #
Misc
mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty Source #
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source #
CoreToLogic
toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap Source #
eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr Source #
Refined Instances
Refined Instances ---------------------------------------------------------
Instances
Functor RInstance Source # | |
Data t => Data (RInstance t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RInstance t -> c (RInstance t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RInstance t) # toConstr :: RInstance t -> Constr # dataTypeOf :: RInstance t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RInstance t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RInstance t)) # gmapT :: (forall b. Data b => b -> b) -> RInstance t -> RInstance t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQ :: (forall d. Data d => d -> u) -> RInstance t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RInstance t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # | |
Generic (RInstance t) Source # | |
Show t => Show (RInstance t) Source # | |
Binary t => Binary (RInstance t) Source # | |
Eq t => Eq (RInstance t) Source # | |
Hashable t => Hashable (RInstance t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint t => PPrint (RInstance t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RInstance t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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)])))) |
Instances
Functor RISig Source # | |
Data t => Data (RISig t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RISig t -> c (RISig t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RISig t) # toConstr :: RISig t -> Constr # dataTypeOf :: RISig t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RISig t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RISig t)) # gmapT :: (forall b. Data b => b -> b) -> RISig t -> RISig t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQ :: (forall d. Data d => d -> u) -> RISig t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RISig t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # | |
Generic (RISig t) Source # | |
Show t => Show (RISig t) Source # | |
Binary t => Binary (RISig t) Source # | |
Eq t => Eq (RISig t) Source # | |
Hashable t => Hashable (RISig t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint t => PPrint (RISig t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RISig t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RISig t) = D1 ('MetaData "RISig" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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))) |
Instances
Functor RILaws Source # | |
Data ty => Data (RILaws ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types 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) # | |
Generic (RILaws ty) Source # | |
Show ty => Show (RILaws ty) Source # | |
Binary t => Binary (RILaws t) Source # | |
Eq ty => Eq (RILaws ty) Source # | |
Hashable ty => Hashable (RILaws ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
PPrint t => PPrint (RILaws t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep (RILaws ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RILaws ty) = D1 ('MetaData "RILaws" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 #
MT | |
|
Instances
Show t => Show (MethodType t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types showsPrec :: Int -> MethodType t -> ShowS # show :: MethodType t -> String # showList :: [MethodType t] -> ShowS # |
getMethodType :: MethodType t -> Maybe t Source #
Ureftable Instances
String Literals
liquidBegin :: String Source #
Values Related to Specifications ------------------------------------
rtyVarType :: RTyVar -> Type Source #
Refined Function Info
Instances
Data RFInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RFInfo -> c RFInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RFInfo # toConstr :: RFInfo -> Constr # dataTypeOf :: RFInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RFInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RFInfo) # gmapT :: (forall b. Data b => b -> b) -> RFInfo -> RFInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> RFInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RFInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # | |
Generic RFInfo Source # | |
Show RFInfo Source # | |
Binary RFInfo Source # | |
NFData RFInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Eq RFInfo Source # | |
Hashable RFInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type Rep RFInfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types |
classRFInfo :: Bool -> RFInfo Source #