| 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
- 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
- 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)
- dropImplicits :: RType c tv r -> RType c tv r
- 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 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, 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
- 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 :: 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
Options
Ghc Information
data TargetVars #
Which Top-Level Binders Should be Verified
Instances
| PPrint TargetVars # | |
Defined in Language.Haskell.Liquid.GHC.Interface | |
Information about Type Constructors
Constructors
| TyConMap | |
F.Located Things
Instances
| Functor Located | |
| Foldable Located | |
Defined in Language.Fixpoint.Types.Spans Methods fold :: Monoid m => Located m -> m # foldMap :: Monoid m => (a -> m) -> Located a -> m # foldMap' :: Monoid m => (a -> m) -> Located a -> m # foldr :: (a -> b -> b) -> b -> Located a -> b # foldr' :: (a -> b -> b) -> b -> Located a -> b # foldl :: (b -> a -> b) -> b -> Located a -> b # foldl' :: (b -> a -> b) -> b -> Located a -> b # foldr1 :: (a -> a -> a) -> Located a -> a # foldl1 :: (a -> a -> a) -> Located a -> a # elem :: Eq a => a -> Located a -> Bool # maximum :: Ord a => Located a -> a # minimum :: Ord a => Located a -> a # | |
| Traversable Located | |
| TyConable LocSymbol # | |
| Qualify BareMeasure # | |
Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure # | |
| Qualify BareSpec # | |
| Qualify ModSpecs # | |
| Eq a => Eq (Located a) | |
| Data a => Data (Located a) | |
Defined in Language.Fixpoint.Types.Spans Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Located a -> c (Located a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Located a) # toConstr :: Located a -> Constr # dataTypeOf :: Located a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Located a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Located a)) # gmapT :: (forall b. Data b => b -> b) -> Located a -> Located a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQ :: (forall d. Data d => d -> u) -> Located a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Located a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # | |
| Ord a => Ord (Located a) | |
| Show a => Show (Located a) | |
| IsString a => IsString (Located a) | |
Defined in Language.Fixpoint.Types.Spans Methods fromString :: String -> Located a # | |
| Generic (Located a) | |
| NFData a => NFData (Located a) | |
Defined in Language.Fixpoint.Types.Spans | |
| Binary a => Binary (Located a) | |
| Symbolic a => Symbolic (Located a) | |
Defined in Language.Fixpoint.Types.Names | |
| Fixpoint a => Fixpoint (Located a) | |
| PPrint a => PPrint (Located a) | |
Defined in Language.Fixpoint.Types.Spans | |
| Expression a => Expression (Located a) | |
Defined in Language.Fixpoint.Types.Refinements | |
| Subable a => Subable (Located a) | |
| Loc (Located a) | |
Defined in Language.Fixpoint.Types.Spans | |
| Hashable a => Hashable (Located a) | |
Defined in Language.Fixpoint.Types.Spans | |
| Qualify a => Qualify (Located a) # | |
| REq r => REq (Located r) # | |
| Binary (Spec LocBareType LocSymbol) # | |
Defined in Language.Haskell.Liquid.Types.Specs | |
| type Rep (Located a) | |
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)))) | |
Symbols
Default unknown name
Bare Type Constructors and Variables
Constructors
| BTyCon | |
Instances
isClassBTyCon :: BTyCon -> Bool #
Constructors
| 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]
Constructors
| TyConInfo | |
Fields
| |
Instances
| Data TyConInfo # | |
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 # | |
| Generic TyConInfo # | |
| NFData TyConInfo # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Default TyConInfo # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify TyConInfo # | |
| type Rep TyConInfo # | |
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))))) | |
rTyConPropVs :: RTyCon -> [PVar RSort] #
isClassType :: TyConable c => RType c t t1 -> Bool #
Refinement Types
Constructors
| RVar | |
| RFun | |
| RImpF | |
| 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.
Constructors
| RProp | |
Instances
| (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) # | |
| SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) # | |
| Functor (Ref τ) # | |
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- |
| (Eq τ, Eq t) => Eq (Ref τ t) # | |
| (Data τ, Data t) => Data (Ref τ t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| (NFData τ, NFData t) => NFData (Ref τ t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Binary τ, Binary t) => Binary (Ref τ t) # | |
| (PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Hashable τ, Hashable t) => Hashable (Ref τ t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| REq t2 => REq (Ref t1 t2) # | |
| PPrint (RTProp c tv r) => Show (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 ()))) => Semigroup (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) # | |
| Reftable (RTProp RTyCon RTyVar ()) | |
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 | |
| Reftable (RTProp RTyCon RTyVar Reft) | |
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 | |
| Reftable (RTProp RTyCon RTyVar (UReft Reft)) | |
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 | |
| Reftable (RTProp BTyCon BTyVar ()) | |
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 | |
| Reftable (RTProp BTyCon BTyVar (UReft Reft)) | |
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 | |
| (Reftable r, TyConable c) => Subable (RTProp c tv r) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (Ref τ t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
type RTProp c tv r = Ref (RType c tv ()) (RType c tv r) #
RTProp is a convenient alias for Ref that will save a bunch of typing.
In general, perhaps we need not expose Ref directly at all.
Instances
Refinement Type Aliases
Constructors
| RTA | |
Instances
| Functor (RTAlias x) # | |
| (Eq x, Eq a) => Eq (RTAlias x a) # | |
| (Data x, Data a) => Data (RTAlias x a) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTAlias x a -> c (RTAlias x a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTAlias x a) # toConstr :: RTAlias x a -> Constr # dataTypeOf :: RTAlias x a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTAlias x a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTAlias x a)) # gmapT :: (forall b. Data b => b -> b) -> RTAlias x a -> RTAlias x a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQ :: (forall d. Data d => d -> u) -> RTAlias x a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTAlias x a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # | |
| (Show tv, Show ty) => Show (RTAlias tv ty) # | Auxiliary Stuff Used Elsewhere --------------------------------------------- |
| Generic (RTAlias x a) # | |
| (Binary x, Binary a) => Binary (RTAlias x a) # | |
| (PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc # | |
| (Hashable x, Hashable a) => Hashable (RTAlias x a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RTAlias x a) # | |
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) #
lmapEAlias :: LMap -> Located (RTAlias Symbol Expr) #
dropImplicits :: RType c tv r -> RType c tv r #
Worlds
Instances
| Data t => Data (HSeg t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| type Rep (HSeg t) # | |
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) # | |
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) # | |
| type Rep (World t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Classes describing operations on RTypes
class Eq c => TyConable c where #
Methods
Instances
Type Variables
Constructors
| RTVar | |
Fields
| |
Instances
| SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) # | |
| SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) # | |
| Eq tv => Eq (RTVar tv s) # | |
| (Data tv, Data s) => Data (RTVar tv s) # | |
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) # | |
| Generic (RTVar tv s) # | |
| (NFData tv, NFData s) => NFData (RTVar tv s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Binary tv, Binary s) => Binary (RTVar tv s) # | |
| PPrint v => PPrint (RTVar v s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Hashable tv, Hashable s) => Hashable (RTVar tv s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RTVar tv s) # | |
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)))) | |
Constructors
| RTVNoInfo | |
Fields
| |
| RTVInfo | |
Fields
| |
Instances
| Functor RTVInfo # | |
| Data s => Data (RTVInfo s) # | |
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) # | |
| NFData s => NFData (RTVInfo s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Binary s => Binary (RTVInfo s) # | |
| Hashable s => Hashable (RTVInfo s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RTVInfo s) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s #
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 #
rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s) #
Predicate Variables
Abstract Predicate Variables ----------------------------------
Constructors
| PV | |
Instances
| Functor PVar # | |
| Subable UsedPVar # | |
| SubsTy tv ty ty => SubsTy tv ty (PVar ty) # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| Eq (PVar t) # | |
| Data t => Data (PVar t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| Show t => Show (PVar t) # | |
| Generic (PVar t) # | |
| NFData t => NFData (PVar t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Binary t => Binary (PVar t) # | |
| PPrint (PVar a) # | F.PPrint ----------------------------------------------------------------- |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable (PVar a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (PVar t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Instances
| Functor PVKind # | |
| Foldable PVKind # | |
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 # elem :: Eq a => a -> PVKind a -> Bool # maximum :: Ord a => PVKind a -> a # minimum :: Ord a => PVKind a -> a # | |
| Traversable PVKind # | |
| SubsTy tv ty ty => SubsTy tv ty (PVKind ty) # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| Data t => Data (PVKind t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| Generic (PVKind t) # | |
| NFData a => NFData (PVKind a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Binary a => Binary (PVKind a) # | |
| type Rep (PVKind t) # | |
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)) | |
Instances
| Eq Predicate # | |
| Data Predicate # | |
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 # | |
| Generic Predicate # | |
| Semigroup Predicate # | |
| Monoid Predicate # | |
| NFData Predicate # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Binary Predicate # | |
| PPrint Predicate # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Reftable Predicate # | |
| Subable Predicate # | |
| Hashable Predicate # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| SubsTy tv RSort Predicate # | |
| SubsTy RTyVar RSort PrType # | |
| type Rep Predicate # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Refinements
Instances
Parse-time entities describing refined data types
Termination expressions
Constructors
| IdSizeFun | x -> F.EVar x |
| SymSizeFun LocSymbol | x -> f x |
Instances
| Data SizeFun # | |
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 # | |
| Generic SizeFun # | |
| NFData SizeFun # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Binary SizeFun # | |
| PPrint SizeFun # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable SizeFun # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify SizeFun # | |
| type Rep SizeFun # | |
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))) | |
Data type refinements
Constructors
| DataDecl | |
Fields
| |
Instances
| Eq DataDecl # | |
| Data DataDecl # | |
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 # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Show DataDecl # | For debugging. |
| Generic DataDecl # | |
| Binary DataDecl # | |
| Symbolic DataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint DataDecl # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| Loc DataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable DataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify DataDecl # | |
| type Rep DataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Constructors
| DnName !LocSymbol | for |
| DnCon !LocSymbol |
Instances
| Eq DataName # | |
| Data DataName # | |
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 # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Show DataName # | |
| Generic DataName # | |
| Binary DataName # | |
| Symbolic DataName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint DataName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Loc DataName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable DataName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep DataName # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep DataName = D1 ('MetaData "DataName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "DnName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol)) :+: C1 ('MetaCons "DnCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol))) | |
dataNameSymbol :: DataName -> LocSymbol #
Data Constructor
Constructors
| DataCtor | |
Instances
| Data DataCtor # | |
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 # | |
| Binary DataCtor # | |
| PPrint DataCtor # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| Loc DataCtor # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable DataCtor # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify DataCtor # | |
| type Rep DataCtor # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Constructors
| DataConP | |
Fields
| |
Instances
| Data DataConP # | |
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 # | |
| Generic DataConP # | |
| PPrint DataConP # | |
Defined in Language.Haskell.Liquid.Types.PredType | |
| Loc DataConP # |
Here the |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep DataConP # | |
Defined in Language.Haskell.Liquid.Types.Types | |
data HasDataDecl #
Instances
| Show HasDataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> HasDataDecl -> ShowS # show :: HasDataDecl -> String # showList :: [HasDataDecl] -> ShowS # | |
| PPrint HasDataDecl # | |
Defined in Language.Haskell.Liquid.Types.Types | |
hasDecl :: DataDecl -> HasDataDecl #
data DataDeclKind #
What kind of DataDecl is it?
Constructors
| DataUser | User defined data-definitions (should have refined fields) |
| DataReflected | Automatically lifted data-definitions (do not have refined fields) |
Instances
Constructors
| TyConP | |
Fields
| |
Instances
Pre-instantiated RType
type RTVU c tv = RTVar tv (RType c tv ()) #
Unified Representation of Refinement Types --------------------------------
Instantiated RType
type LocBareType = Located BareType #
type LocSpecType = Located SpecType #
Predicates ----------------------------------------------------------------
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
Constructors
| REnv | |
Constructing & Destructing RTypes
Constructor and Destructors for RTypes ------------------------------------
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 #
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 #
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 #
mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft #
Visitors ------------------------------------------------------------------
???
Different kinds of Check Obligations ------------------------------------
Constructors
| OTerm | Obligation that proves termination |
| OInv | Obligation that proves invariants |
| OCons | Obligation that proves subtyping constraints |
Instances
| Eq Oblig # | |
| Data Oblig # | |
Defined in Language.Haskell.Liquid.Types.Errors Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Oblig -> c Oblig # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Oblig # 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 # | |
| Generic Oblig # | |
| NFData Oblig # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| Binary Oblig # | |
| PPrint Oblig # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| Hashable Oblig # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| type Rep Oblig # | |
Defined in Language.Haskell.Liquid.Types.Errors type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type))) | |
ignoreOblig :: RType t t1 t2 -> RType t t1 t2 #
addInvCond :: SpecType -> RReft -> SpecType #
Inferred Annotations
Annotations -------------------------------------------------------
Instances
| Functor AnnInfo # | |
| Data a => Data (AnnInfo a) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnInfo a -> c (AnnInfo a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AnnInfo a) # toConstr :: AnnInfo a -> Constr # dataTypeOf :: AnnInfo a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AnnInfo a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AnnInfo a)) # gmapT :: (forall b. Data b => b -> b) -> AnnInfo a -> AnnInfo a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQ :: (forall d. Data d => d -> u) -> AnnInfo a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnInfo a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # | |
| PPrint a => Show (AnnInfo a) # | |
| Generic (AnnInfo a) # | |
| Semigroup (AnnInfo a) # | |
| Monoid (AnnInfo a) # | |
| NFData a => NFData (AnnInfo a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint a => PPrint (AnnInfo a) # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| FromJSON a => FromJSON (AnnInfo a) | |
Defined in Language.Haskell.Liquid.UX.DiffCheck | |
| ToJSON a => ToJSON (AnnInfo a) | |
Defined in Language.Haskell.Liquid.UX.DiffCheck Methods toEncoding :: AnnInfo a -> Encoding toJSONList :: [AnnInfo a] -> Value toEncodingList :: [AnnInfo a] -> Encoding | |
| type Rep (AnnInfo a) # | |
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)])))) | |
Instances
| Functor Annot # | |
| Data t => Data (Annot t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot t -> c (Annot t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Annot t) # toConstr :: Annot t -> Constr # dataTypeOf :: Annot t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Annot t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Annot t)) # gmapT :: (forall b. Data b => b -> b) -> Annot t -> Annot t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQ :: (forall d. Data d => d -> u) -> Annot t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # | |
| Generic (Annot t) # | |
| NFData a => NFData (Annot a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint t => PPrint (Annot t) # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| type Rep (Annot t) # | |
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
Var Hole Info -----------------------------------------------------
Overall Output
Output --------------------------------------------------------------------
Constructors
| O | |
Instances
Refinement Hole
Converting To and From Sort
rTypeValueVar :: Reftable r => RType c tv r -> Symbol #
stripRTypeBase :: RType c tv r -> Maybe r #
topRTypeBase :: Reftable r => RType c tv r -> RType c tv r #
Class for values that can be pretty printed
Minimal complete definition
Nothing
Instances
Printer Configuration
Printer ----------------------------------------------------------------
Constructors
| PP | |
ppEnvShort :: PPEnv -> PPEnv #
Modules and Imports
Module Names --------------------------------------------------------------
Constructors
| ModName !ModType !ModuleName |
Instances
| Eq ModName # | |
| Data ModName # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModName -> c ModName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModName # toConstr :: ModName -> Constr # dataTypeOf :: ModName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModName) # gmapT :: (forall b. Data b => b -> b) -> ModName -> ModName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQ :: (forall d. Data d => d -> u) -> ModName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName # | |
| Ord ModName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Show ModName # | |
| Generic ModName # | |
| Symbolic ModName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint ModName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable ModName # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify ModSpecs # | |
| type Rep ModName # | |
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))) | |
Constructors
| Target | |
| SrcImport | |
| SpecImport |
Instances
| Eq ModType # | |
| Data ModType # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModType -> c ModType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModType # toConstr :: ModType -> Constr # dataTypeOf :: ModType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModType) # gmapT :: (forall b. Data b => b -> b) -> ModType -> ModType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQ :: (forall d. Data d => d -> u) -> ModType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # | |
| Ord ModType # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Show ModType # | |
| Generic ModType # | |
| Hashable ModType # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep ModType # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep ModType = D1 ('MetaData "ModType" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "Target" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SrcImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpecImport" 'PrefixI 'False) (U1 :: Type -> Type))) | |
isSrcImport :: ModName -> Bool #
isSpecImport :: ModName -> Bool #
getModName :: ModName -> ModuleName #
getModString :: ModName -> String #
qualifyModName :: ModName -> Symbol -> Symbol #
Refinement Type Aliases
Refinement Type Aliases ---------------------------------------------------
Constructors
| RTE | |
Fields
| |
type BareRTAlias = RTAlias Symbol BareType #
type SpecRTAlias = RTAlias RTyVar SpecType #
Diagnostics, Warnings, Errors and Error Messages
type ErrorResult = FixResult UserError #
Error Data Type -----------------------------------------------------------
Diagnostic info -----------------------------------------------------------
data Diagnostics #
Instances
| Eq Diagnostics # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Semigroup Diagnostics # | |
Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: Diagnostics -> Diagnostics -> Diagnostics # sconcat :: NonEmpty Diagnostics -> Diagnostics # stimes :: Integral b => b -> Diagnostics -> Diagnostics # | |
| Monoid Diagnostics # | |
Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: Diagnostics # mappend :: Diagnostics -> Diagnostics -> Diagnostics # mconcat :: [Diagnostics] -> Diagnostics # | |
mkDiagnostics :: [Warning] -> [Error] -> Diagnostics #
noErrors :: Diagnostics -> Bool #
allWarnings :: Diagnostics -> [Warning] #
allErrors :: Diagnostics -> [Error] #
printWarning :: DynFlags -> Warning -> IO () #
Printing Warnings ---------------------------------------------------------
Source information (associated with constraints)
Source Information Associated With Constraints ----------------------------
Instances
| Eq Cinfo # | |
| Ord Cinfo # | |
| Show Cinfo # | |
| Generic Cinfo # | |
| NFData Cinfo # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Fixpoint Cinfo # | |
| Loc Cinfo # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Result (FixResult Cinfo) # | |
Defined in Language.Haskell.Liquid.UX.Tidy | |
| type Rep Cinfo # | |
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
Constructors
| M | |
Fields
| |
Instances
| Bifunctor Measure # | |
| Qualify BareMeasure # | |
Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure # | |
| Functor (Measure ty) # | |
| (Eq ty, Eq ctor) => Eq (Measure ty ctor) # | |
| (Data ty, Data ctor) => Data (Measure ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| Generic (Measure ty ctor) # | |
| (Binary t, Binary c) => Binary (Measure t c) # | |
| (PPrint t, PPrint a) => PPrint (Measure t a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Subable (Measure ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Loc (Measure a b) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Hashable ty, Hashable ctor) => Hashable (Measure ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify (Measure SpecType DataCon) # | |
| type Rep (Measure ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (Measure ty ctor) = D1 ('MetaData "Measure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :*: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Def ty ctor]) :*: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :*: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs))))) | |
type UnSortedExprs = [UnSortedExpr] #
type UnSortedExpr = ([Symbol], Expr) #
data MeasureKind #
Constructors
| MsReflect | due to `reflect foo` |
| MsMeasure | due to `measure foo` with old-style (non-haskell) equations |
| MsLifted | due to `measure foo` with new-style haskell equations |
| MsClass | due to `class measure` definition |
| MsAbsMeasure | due to `measure foo` without equations c.f. testsposT1223.hs |
| MsSelector | due to selector-fields e.g. `data Foo = Foo { fld :: Int }` |
| MsChecker | due to checkers e.g. `is-F` for `data Foo = F ... | G ...` |
Instances
Instances
| Functor CMeasure # | |
| Data ty => Data (CMeasure ty) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMeasure ty -> c (CMeasure ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CMeasure ty) # toConstr :: CMeasure ty -> Constr # dataTypeOf :: CMeasure ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CMeasure ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CMeasure ty)) # gmapT :: (forall b. Data b => b -> b) -> CMeasure ty -> CMeasure ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQ :: (forall d. Data d => d -> u) -> CMeasure ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CMeasure ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # | |
| PPrint (CMeasure t) => Show (CMeasure t) # | |
| Generic (CMeasure ty) # | |
| PPrint t => PPrint (CMeasure t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (CMeasure ty) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (CMeasure ty) = D1 ('MetaData "CMeasure" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-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))) | |
Constructors
| Def | |
Instances
| Bifunctor Def # | |
| Functor (Def ty) # | |
| (Eq ctor, Eq ty) => Eq (Def ty ctor) # | |
| (Data ty, Data ctor) => Data (Def ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| Generic (Def ty ctor) # | |
| (Binary t, Binary c) => Binary (Def t c) # | |
| PPrint a => PPrint (Def t a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Subable (Def ty ctor) # | |
| (Hashable ctor, Hashable ty) => Hashable (Def ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify (Def ty ctor) # | |
| type Rep (Def ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Measures
Constructors
| E Expr | Measure Refinement: {v | v = e } |
| P Expr | Measure Refinement: {v | (? v) = p } |
| R Symbol Expr | Measure Refinement: {v | p} |
Instances
| Eq Body # | |
| Data Body # | |
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 # 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 # | |
| Generic Body # | |
| Binary Body # | |
| PPrint Body # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Subable Body # | |
| Hashable Body # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Qualify Body # | |
| type Rep Body # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Constructors
| MSpec | |
Instances
| Bifunctor MSpec # | |
| Functor (MSpec ty) # | |
| (Data ty, Data ctor) => Data (MSpec ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) # toConstr :: MSpec ty ctor -> Constr # dataTypeOf :: MSpec ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # | |
| (Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) # | |
| Generic (MSpec ty ctor) # | |
| Eq ctor => Semigroup (MSpec ty ctor) # | |
| Eq ctor => Monoid (MSpec ty ctor) # | |
| (PPrint t, PPrint a) => PPrint (MSpec t a) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (MSpec ty ctor) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
Scoping Info
Type Classes
Constructors
| RClass | |
Instances
| Functor RClass # | |
| Eq ty => Eq (RClass ty) # | |
| Data ty => Data (RClass ty) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RClass ty -> c (RClass ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RClass ty) # toConstr :: RClass ty -> Constr # dataTypeOf :: RClass ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RClass ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RClass ty)) # gmapT :: (forall b. Data b => b -> b) -> RClass ty -> RClass ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQ :: (forall d. Data d => d -> u) -> RClass ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RClass ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # | |
| Show ty => Show (RClass ty) # | |
| Generic (RClass ty) # | |
| Binary ty => Binary (RClass ty) # | |
| PPrint t => PPrint (RClass t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable ty => Hashable (RClass ty) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RClass ty) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RClass ty) = D1 ('MetaData "RClass" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-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
KVar Profile --------------------------------------------------------------
Constructors
| RecBindE Var | Recursive binder |
| NonRecBindE Var | Non recursive binder |
| TypeInstE | |
| PredInstE | |
| LamE | |
| CaseE Int | Int is the number of cases |
| LetE | |
| ImplictE | |
| ProjectE | Projecting out field of |
Instances
| Eq KVKind # | |
| Data KVKind # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVKind -> c KVKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVKind # toConstr :: KVKind -> Constr # dataTypeOf :: KVKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVKind) # gmapT :: (forall b. Data b => b -> b) -> KVKind -> KVKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQ :: (forall d. Data d => d -> u) -> KVKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KVKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # | |
| Ord KVKind # | |
| Show KVKind # | |
| Generic KVKind # | |
| NFData KVKind # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint KVKind # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable KVKind # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep KVKind # | |
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))))) | |
Instances
| Generic KVProf # | |
| NFData KVProf # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint KVProf # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep KVProf # | |
Defined in Language.Haskell.Liquid.Types.Types | |
emptyKVProf :: KVProf #
Misc
mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty #
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a #
CoreToLogic
Constructors
| LM | |
toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap #
eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr #
Refined Instances
Refined Instances ---------------------------------------------------------
Instances
| Functor RInstance # | |
| Eq t => Eq (RInstance t) # | |
| Data t => Data (RInstance t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RInstance t -> c (RInstance t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RInstance t) # toConstr :: RInstance t -> Constr # dataTypeOf :: RInstance t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RInstance t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RInstance t)) # gmapT :: (forall b. Data b => b -> b) -> RInstance t -> RInstance t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQ :: (forall d. Data d => d -> u) -> RInstance t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RInstance t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # | |
| Show t => Show (RInstance t) # | |
| Generic (RInstance t) # | |
| Binary t => Binary (RInstance t) # | |
| PPrint t => PPrint (RInstance t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable t => Hashable (RInstance t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RInstance t) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RInstance t) = D1 ('MetaData "RInstance" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-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)])))) | |
Instances
| Functor RISig # | |
| Eq t => Eq (RISig t) # | |
| Data t => Data (RISig t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RISig t -> c (RISig t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RISig t) # toConstr :: RISig t -> Constr # dataTypeOf :: RISig t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RISig t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RISig t)) # gmapT :: (forall b. Data b => b -> b) -> RISig t -> RISig t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQ :: (forall d. Data d => d -> u) -> RISig t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RISig t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # | |
| Show t => Show (RISig t) # | |
| Generic (RISig t) # | |
| Binary t => Binary (RISig t) # | |
| PPrint t => PPrint (RISig t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable t => Hashable (RISig t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RISig t) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RISig t) = D1 ('MetaData "RISig" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-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))) | |
Constructors
| RIL | |
Instances
| Functor RILaws # | |
| Eq ty => Eq (RILaws ty) # | |
| Data ty => Data (RILaws ty) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) # | |
| Generic (RILaws ty) # | |
| Binary t => Binary (RILaws t) # | |
| PPrint t => PPrint (RILaws t) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| Hashable ty => Hashable (RILaws ty) # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (RILaws ty) # | |
Defined in Language.Haskell.Liquid.Types.Types type Rep (RILaws ty) = D1 ('MetaData "RILaws" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "RIL" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rilName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "rilSupers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty])) :*: (S1 ('MetaSel ('Just "rilTyArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ty]) :*: (S1 ('MetaSel ('Just "rilEqus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(LocSymbol, LocSymbol)]) :*: S1 ('MetaSel ('Just "rilPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located ())))))) | |
data MethodType t #
Constructors
| MT | |
Fields
| |
Instances
| Show t => Show (MethodType t) # | |
Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MethodType t -> ShowS # show :: MethodType t -> String # showList :: [MethodType t] -> ShowS # | |
getMethodType :: MethodType t -> Maybe t #
Ureftable Instances
String Literals
liquidBegin :: String #
Values Related to Specifications ------------------------------------
Constructors
| Axiom | |
rtyVarType :: RTyVar -> Type #
Orphan instances
| Ord DataCon # | |
| Ord TyCon # | |
| Show DataCon # | |
| Show ModuleName # | |
Methods showsPrec :: Int -> ModuleName -> ShowS # show :: ModuleName -> String # showList :: [ModuleName] -> ShowS # | |
| Symbolic DataCon # | |
| Symbolic ModuleName # | |
Methods symbol :: ModuleName -> Symbol | |
| PPrint DataCon # | |
| PPrint TyThing # | |
| Hashable ModuleName # | |
| NFData a => NFData (TError a) # | |
| Subable t => Subable (WithModel t) # | |