| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.Types
Contents
- Ghc Information
- F.Located Things
- Symbols
- Default unknown name
- Refinement Types
- Classes describing operations on
RTypes - Relational predicates
- Pre-instantiated RType
- ???
- Inferred Annotations
- Hole Information
- Overall Output
- Refinement Hole
- Class for values that can be pretty printed
- Modules and Imports
- Refinement Type Aliases
- Diagnostics, Warnings, Errors and Error Messages
- Source information (associated with constraints)
- Measures
- Type Classes
- KV Profiling
- Misc
- CoreToLogic
- Refined Instances
- String Literals
- Orphan instances
Description
Core types
Synopsis
- 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 RTAlias x a = RTA {}
- lmapEAlias :: LMap -> RTAlias Symbol Expr
- class Eq c => TyConable c where
- class SubsTy tv ty a where
- subt :: (tv, ty) -> a -> a
- type RelExpr = RelExprV Symbol
- data RelExprV v
- = ERBasic (ExprV v)
- | ERChecked (ExprV v) (RelExprV v)
- | ERUnChecked (ExprV v) (RelExprV v)
- type REnv = AREnv SpecType
- data AREnv t = REnv {}
- data Oblig
- ignoreOblig :: RTypeBV b v c tv r -> RTypeBV b v c tv r
- newtype AnnInfo a = AI (HashMap SrcSpan [(Maybe Text, a)])
- data Annot t
- data HoleInfo i t = HoleInfo {}
- data Output a = O {}
- hole :: ExprV v
- isHole :: Expr -> Bool
- hasHole :: (ToReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => r -> Bool
- class PPrint a where
- pprintTidy :: Tidy -> a -> Doc
- pprintPrec :: Int -> Tidy -> a -> Doc
- pprint :: PPrint a => a -> Doc
- showpp :: PPrint a => a -> String
- data ModName = ModName !ModType !ModuleName
- data ModType
- isSrcImport :: ModName -> Bool
- isSpecImport :: ModName -> Bool
- isTarget :: ModName -> Bool
- getModName :: ModName -> ModuleName
- getModString :: ModName -> String
- data RTEnv tv t = RTE {
- typeAliases :: HashMap LHName (RTAlias tv t)
- exprAliases :: HashMap LHName (RTAlias Symbol Expr)
- type BareRTEnv = RTEnv Symbol BareType
- type SpecRTEnv = RTEnv RTyVar SpecType
- type BareRTAlias = RTAlias Symbol BareType
- type SpecRTAlias = RTAlias RTyVar SpecType
- 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 -> Warning -> IO ()
- data Cinfo = Ci {}
- type Measure ty ctor = MeasureV Symbol ty ctor
- data MeasureV v ty ctor = M {
- msName :: Located LHName
- msSort :: ty
- msEqns :: [DefV v ty ctor]
- msKind :: !MeasureKind
- msUnSorted :: !UnSortedExprs
- type UnSortedExprs = [UnSortedExpr]
- type UnSortedExpr = ([Symbol], Expr)
- data MeasureKind
- data CMeasure ty = CM {}
- type Def ty ctor = DefV Symbol ty ctor
- data DefV v ty ctor = Def {}
- type Body = BodyV Symbol
- data BodyV v
- data MSpec ty ctor = MSpec {}
- mapDefTy :: (ty0 -> ty1) -> DefV v ty0 ctor -> DefV v ty1 ctor
- mapMeasureTy :: (ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor
- emapDefM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> DefV v0 ty0 ctor -> m (DefV v1 ty1 ctor)
- mapDefV :: (v -> v') -> DefV v ty ctor -> DefV v' ty ctor
- mapMeasureV :: (v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor
- emapMeasureM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> MeasureV v0 ty0 ctor -> m (MeasureV v1 ty1 ctor)
- emapRelExprV :: Monad m => ([Symbol] -> v0 -> m v1) -> RelExprV v0 -> m (RelExprV v1)
- data RClass ty = RClass {}
- data KVKind
- data KVProf
- emptyKVProf :: KVProf
- updKVProf :: KVKind -> Kuts -> KVProf -> KVProf
- mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty
- data LogicMap = LM {}
- toLMapV :: (Located LHName, ([Symbol], ExprV v)) -> (Located LHName, LMapV v)
- mkLogicMap :: HashMap Symbol LMap -> LogicMap
- toLogicMap :: [(LocSymbol, ([Symbol], Expr))] -> LogicMap
- eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
- emapLMapM :: Monad m => ([Symbol] -> v0 -> m v1) -> LMapV v0 -> m (LMapV v1)
- data LMapV v = LMap {}
- type LMap = LMapV Symbol
- type RDEnv = DEnv Var SpecType
- newtype DEnv x ty = DEnv (HashMap x (HashMap Symbol (RISig ty)))
- data RInstance t = RI {}
- data RISig t
- data MethodType t = MT {
- tyInstance :: !(Maybe t)
- tyClass :: !(Maybe t)
- getMethodType :: MethodType t -> Maybe t
- liquidBegin :: String
- liquidEnd :: String
- data Axiom b s e = Axiom {}
- type HAxiom = Axiom Var Type CoreExpr
- ordSrcSpan :: SrcSpan -> SrcSpan -> Ordering
Ghc Information
Information about Type Constructors
Constructors
| TyConMap | |
F.Located Things
Instances
Symbols
Default unknown name
Refinement Types
Refinement Type and Expression Aliases
Constructors
| RTA | |
Instances
| Expand BareRTAlias Source # | |||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source # | |||||
| Functor (RTAlias x) Source # | |||||
| Foldable (RTAlias x) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => RTAlias x m -> m # foldMap :: Monoid m => (a -> m) -> RTAlias x a -> m # foldMap' :: Monoid m => (a -> m) -> RTAlias x a -> m # foldr :: (a -> b -> b) -> b -> RTAlias x a -> b # foldr' :: (a -> b -> b) -> b -> RTAlias x a -> b # foldl :: (b -> a -> b) -> b -> RTAlias x a -> b # foldl' :: (b -> a -> b) -> b -> RTAlias x a -> b # foldr1 :: (a -> a -> a) -> RTAlias x a -> a # foldl1 :: (a -> a -> a) -> RTAlias x a -> a # toList :: RTAlias x a -> [a] # length :: RTAlias x a -> Int # elem :: Eq a => a -> RTAlias x a -> Bool # maximum :: Ord a => RTAlias x a -> a # minimum :: Ord a => RTAlias x a -> a # | |||||
| Traversable (RTAlias x) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (Binary x, Binary a) => Binary (RTAlias x a) Source # | |||||
| (Eq x, Eq a) => Eq (RTAlias x a) Source # | |||||
| (Data x, Data a) => Data (RTAlias x a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTAlias x a -> c (RTAlias x a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTAlias x a) # toConstr :: RTAlias x a -> Constr # dataTypeOf :: RTAlias x a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTAlias x a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTAlias x a)) # gmapT :: (forall b. Data b => b -> b) -> RTAlias x a -> RTAlias x a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTAlias x a -> r # gmapQ :: (forall d. Data d => d -> u) -> RTAlias x a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTAlias x a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTAlias x a -> m (RTAlias x a) # | |||||
| Generic (RTAlias x a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (Show tv, Show ty) => Show (RTAlias tv ty) Source # | Auxiliary Stuff Used Elsewhere --------------------------------------------- | ||||
| (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 Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc # | |||||
| Expand (RTAlias Symbol Expr) Source # | |||||
| type Rep (RTAlias x a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (RTAlias x a) = D1 ('MetaData "RTAlias" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "RTA" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "rtTArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [x])) :*: (S1 ('MetaSel ('Just "rtVArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "rtBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) | |||||
lmapEAlias :: LMap -> RTAlias Symbol Expr Source #
Classes describing operations on RTypes
class Eq c => TyConable c where Source #
Methods
isEmbeddedDict :: c -> Bool Source #
isOrdCls :: c -> Bool Source #
Instances
| TyConable TyCon Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: TyCon -> Bool Source # isList :: TyCon -> Bool Source # isTuple :: TyCon -> Bool Source # ppTycon :: TyCon -> Doc Source # isClass :: TyCon -> Bool Source # isEmbeddedDict :: TyCon -> Bool Source # isEqual :: TyCon -> Bool Source # isOrdCls :: TyCon -> Bool Source # isEqCls :: TyCon -> Bool Source # | |
| TyConable LocSymbol Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: LocSymbol -> Bool Source # isList :: LocSymbol -> Bool Source # isTuple :: LocSymbol -> Bool Source # ppTycon :: LocSymbol -> Doc Source # isClass :: LocSymbol -> Bool Source # isEmbeddedDict :: LocSymbol -> Bool Source # isEqual :: LocSymbol -> Bool Source # isOrdCls :: LocSymbol -> Bool Source # isEqCls :: LocSymbol -> Bool Source # | |
| TyConable Symbol Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: Symbol -> Bool Source # isList :: Symbol -> Bool Source # isTuple :: Symbol -> Bool Source # ppTycon :: Symbol -> Doc Source # isClass :: Symbol -> Bool Source # isEmbeddedDict :: Symbol -> Bool Source # isEqual :: Symbol -> Bool Source # isOrdCls :: Symbol -> Bool Source # isEqCls :: Symbol -> Bool Source # | |
| TyConable BTyCon Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: BTyCon -> Bool Source # isList :: BTyCon -> Bool Source # isTuple :: BTyCon -> Bool Source # ppTycon :: BTyCon -> Doc Source # isClass :: BTyCon -> Bool Source # isEmbeddedDict :: BTyCon -> Bool Source # isEqual :: BTyCon -> Bool Source # isOrdCls :: BTyCon -> Bool Source # isEqCls :: BTyCon -> Bool Source # | |
| TyConable RTyCon Source # | TyConable Instances ------------------------------------------------------- |
Defined in Language.Haskell.Liquid.Types.RType Methods isFun :: RTyCon -> Bool Source # isList :: RTyCon -> Bool Source # isTuple :: RTyCon -> Bool Source # ppTycon :: RTyCon -> Doc Source # isClass :: RTyCon -> Bool Source # isEmbeddedDict :: RTyCon -> Bool Source # isEqual :: RTyCon -> Bool Source # isOrdCls :: RTyCon -> Bool Source # isEqCls :: RTyCon -> Bool Source # | |
class SubsTy tv ty a where Source #
Instances
| SubsTy TyVar Type SpecType Source # | |
| SubsTy Symbol RSort Sort Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| SubsTy BTyVar BSort BSort Source # | |
| SubsTy BTyVar BSort BTyCon Source # | |
| SubsTy RTyVar RSort Sort Source # | |
| SubsTy RTyVar RSort RSort Source # | |
| SubsTy RTyVar RSort RTyCon Source # | |
| SubsTy RTyVar RSort SpecType Source # | |
| SubsTy RTyVar RTyVar SpecType Source # | |
| SubsTy tv RSort Predicate Source # | |
| SubsTy tv ty Symbol Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| SubsTy tv ty Sort => SubsTy tv ty Expr Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| SubsTy tv ty Expr => SubsTy tv ty Reft Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| SubsTy tv ty NoReft Source # | |
| SubsTy Symbol Symbol (BRType r) Source # | |
| SubsTy tv ty r => SubsTy tv ty (UReft r) Source # | |
| (SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) Source # | |
Defined in Language.Haskell.Liquid.Types.RefType | |
| SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # | |
| SubsTy tv ty ty => SubsTy tv ty (PVarBV b v ty) Source # | |
| (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv NoReft)) => SubsTy tv ty (RTProp c tv (UReft r)) Source # | |
| SubsTy BTyVar (RType BTyCon BTyVar NoReft) Sort Source # | |
| SubsTy BTyVar (RType c BTyVar NoReft) BTyVar Source # | |
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) RTyVar Source # | |
| SubsTy BTyVar (RType c BTyVar NoReft) (RTVar BTyVar (RType c BTyVar NoReft)) Source # | |
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) (RTVar RTyVar (RType RTyCon RTyVar NoReft)) Source # | |
Relational predicates
type RelExpr = RelExprV Symbol Source #
Relational predicates --------------------------------------------------
Constructors
| ERBasic (ExprV v) | |
| ERChecked (ExprV v) (RelExprV v) | |
| ERUnChecked (ExprV v) (RelExprV v) |
Instances
| Functor RelExprV Source # | |||||
| Foldable RelExprV Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => RelExprV m -> m # foldMap :: Monoid m => (a -> m) -> RelExprV a -> m # foldMap' :: Monoid m => (a -> m) -> RelExprV a -> m # foldr :: (a -> b -> b) -> b -> RelExprV a -> b # foldr' :: (a -> b -> b) -> b -> RelExprV a -> b # foldl :: (b -> a -> b) -> b -> RelExprV a -> b # foldl' :: (b -> a -> b) -> b -> RelExprV a -> b # foldr1 :: (a -> a -> a) -> RelExprV a -> a # foldl1 :: (a -> a -> a) -> RelExprV a -> a # elem :: Eq a => a -> RelExprV a -> Bool # maximum :: Ord a => RelExprV a -> a # minimum :: Ord a => RelExprV a -> a # | |||||
| Traversable RelExprV Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| PPrint RelExpr Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Binary v => Binary (RelExprV v) Source # | |||||
| Eq v => Eq (RelExprV v) Source # | |||||
| Data v => Data (RelExprV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelExprV v -> c (RelExprV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RelExprV v) # toConstr :: RelExprV v -> Constr # dataTypeOf :: RelExprV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RelExprV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RelExprV v)) # gmapT :: (forall b. Data b => b -> b) -> RelExprV v -> RelExprV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelExprV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelExprV v -> r # gmapQ :: (forall d. Data d => d -> u) -> RelExprV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RelExprV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelExprV v -> m (RelExprV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExprV v -> m (RelExprV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelExprV v -> m (RelExprV v) # | |||||
| Generic (RelExprV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (Show v, Ord v, Fixpoint v) => Show (RelExprV v) Source # | |||||
| type Rep (RelExprV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (RelExprV v) = D1 ('MetaData "RelExprV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "ERBasic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "ERChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v))) :+: C1 ('MetaCons "ERUnChecked" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RelExprV v))))) | |||||
Pre-instantiated RType
type REnv = AREnv SpecType 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
Constructors
| REnv | |
???
Different kinds of Check Obligations ------------------------------------
Constructors
| OTerm | Obligation that proves termination |
| OInv | Obligation that proves invariants |
| OCons | Obligation that proves subtyping constraints |
Instances
| Binary Oblig Source # | |||||
| NFData Oblig Source # | |||||
Defined in Language.Haskell.Liquid.Types.Errors | |||||
| Eq Oblig Source # | |||||
| Data Oblig Source # | |||||
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 # | |||||
| Generic Oblig Source # | |||||
Defined in Language.Haskell.Liquid.Types.Errors Associated Types
| |||||
| Show 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.14.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 :: RTypeBV b v c tv r -> RTypeBV b v c tv r Source #
Inferred Annotations
Annotations -------------------------------------------------------
Instances
| Functor AnnInfo Source # | |||||
| FromJSON a => FromJSON (AnnInfo a) Source # | |||||
Defined in Language.Haskell.Liquid.UX.DiffCheck | |||||
| ToJSON a => ToJSON (AnnInfo a) Source # | |||||
| NFData a => NFData (AnnInfo a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Monoid (AnnInfo a) Source # | |||||
| Semigroup (AnnInfo a) Source # | |||||
| Data a => Data (AnnInfo a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnInfo a -> c (AnnInfo a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AnnInfo a) # toConstr :: AnnInfo a -> Constr # dataTypeOf :: AnnInfo a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AnnInfo a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AnnInfo a)) # gmapT :: (forall b. Data b => b -> b) -> AnnInfo a -> AnnInfo a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnInfo a -> r # gmapQ :: (forall d. Data d => d -> u) -> AnnInfo a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnInfo a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnInfo a -> m (AnnInfo a) # | |||||
| Generic (AnnInfo a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| PPrint a => Show (AnnInfo a) Source # | |||||
| 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.14.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 Source # | |||||
| NFData a => NFData (Annot a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Data t => Data (Annot t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot t -> c (Annot t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Annot t) # toConstr :: Annot t -> Constr # dataTypeOf :: Annot t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Annot t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Annot t)) # gmapT :: (forall b. Data b => b -> b) -> Annot t -> Annot t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot t -> r # gmapQ :: (forall d. Data d => d -> u) -> Annot t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot t -> m (Annot t) # | |||||
| Generic (Annot t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated 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.14.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 -----------------------------------------------------
Information captured for a term hole: the type reported at the hole, its source location, the local typing environment, and extra caller-provided context.
Overall Output
Output --------------------------------------------------------------------
Constructors
| O | |
Instances
| Functor Output Source # | |||||
| FromJSON (Output Doc) Source # | |||||
| ToJSON (Output Doc) Source # | |||||
| Monoid (Output a) Source # | |||||
| Semigroup (Output a) Source # | |||||
| Generic (Output a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| PPrint a => PPrint (Output a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Rep (Output a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (Output a) = D1 ('MetaData "Output" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "O" 'PrefixI 'True) ((S1 ('MetaSel ('Just "o_vars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [String])) :*: S1 ('MetaSel ('Just "o_types") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a))) :*: (S1 ('MetaSel ('Just "o_templs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (AnnInfo a)) :*: (S1 ('MetaSel ('Just "o_bots") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]) :*: S1 ('MetaSel ('Just "o_result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErrorResult))))) | |||||
Refinement Hole
Class for values that can be pretty printed
Minimal complete definition
Nothing
Instances
| PPrint Class Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint DataCon Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl | |
| PPrint Type Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint TyCon Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint Name Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint SourceError Source # | A whole bunch of PPrint instances follow ---------------------------------- |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint SrcSpan Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| PPrint TyThing Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint Var Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint CVertex # | |
Defined in Language.Fixpoint.Graph.Types | |
| PPrint KVGraph # | |
Defined in Language.Fixpoint.Graph.Types | |
| PPrint Rank # | |
Defined in Language.Fixpoint.Graph.Types | |
| PPrint Pred # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint Tag # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint Command # | |
Defined in Language.Fixpoint.Smt.Types | |
| PPrint TermOrigin # | |
Defined in Language.Fixpoint.Solver.Rewrite | |
| PPrint WorkItem # | |
Defined in Language.Fixpoint.Solver.Worklist | |
| PPrint AxiomEnv # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint DefinedFuns # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint Equation # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint QualParam # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint QualPattern # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint Rewrite # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint IBindEnv # | |
Defined in Language.Fixpoint.Types.Environments | |
| PPrint Packs # | |
Defined in Language.Fixpoint.Types.Environments | |
| PPrint Error # | |
Defined in Language.Fixpoint.Types.Errors | |
| PPrint Error1 # | |
Defined in Language.Fixpoint.Types.Errors | |
| PPrint Symbol # | |
Defined in Language.Fixpoint.Types.Names | |
| PPrint DocTable # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Tidy Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint Bop # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint Brel # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint Constant # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint KVSub # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint KVar # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint SortedReft # | |
Defined in Language.Fixpoint.Types.Substitutions | |
| PPrint SymConst # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint BIndex # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint BindPred # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint Cube # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint EQual # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint KIndex # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint QBind # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint DataCtor # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint DataDecl # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint DataField # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint FTycon # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint Sort # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint TCArgs # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint SrcSpan # | |
Defined in Language.Fixpoint.Types.Spans | |
| PPrint Templates # | |
Defined in Language.Fixpoint.Types.Templates | |
| PPrint Sem # | |
Defined in Language.Fixpoint.Types.Theories | |
| PPrint SmtSort # | |
Defined in Language.Fixpoint.Types.Theories | |
| PPrint TheorySymbol # | |
Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> TheorySymbol -> Doc # pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc # | |
| PPrint Trigger # | |
Defined in Language.Fixpoint.Types.Triggers | |
| PPrint Stats # | |
Defined in Language.Fixpoint.Utils.Statistics | |
| PPrint CGEnv Source # | |
Defined in Language.Haskell.Liquid.Constraint.Types | |
| PPrint CGInfo Source # | |
Defined in Language.Haskell.Liquid.Constraint.Types | |
| PPrint SubC Source # | |
Defined in Language.Haskell.Liquid.Constraint.Types | |
| PPrint WfC Source # | |
Defined in Language.Haskell.Liquid.Constraint.Types | |
| PPrint Pattern Source # | |
Defined in Language.Haskell.Liquid.GHC.Resugar | |
| PPrint BPspec Source # | |
Defined in Language.Haskell.Liquid.Parse | |
| PPrint SpecType => PPrint DataConP Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl | |
| PPrint DataName Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl | |
| PPrint HasDataDecl Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl | |
| PPrint Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| PPrint ParseError Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| PPrint UserError Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| PPrint LHName Source # | |
Defined in Language.Haskell.Liquid.Types.Names | |
| PPrint BTyCon Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint BTyVar Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint RTyCon Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint RTyVar Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint TyConP Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint TargetInfo Source # | |
Defined in Language.Haskell.Liquid.GHC.Interface | |
| PPrint TargetSpec Source # | Pretty Printing ----------------------------------------------------------- |
Defined in Language.Haskell.Liquid.GHC.Interface | |
| PPrint Cinfo Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint Error Source # | |
Defined in Language.Haskell.Liquid.UX.Tidy | |
| PPrint KVKind Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint KVProf Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint LogicMap Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint ModName Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint RelExpr Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint Variance Source # | |
Defined in Language.Haskell.Liquid.Types.Variance | |
| PPrint Def Source # | |
Defined in Language.Haskell.Liquid.UX.DiffCheck | |
| PPrint DiffCheck Source # | |
Defined in Language.Haskell.Liquid.UX.DiffCheck | |
| PPrint SourcePos # | |
Defined in Language.Fixpoint.Types.Spans | |
| PPrint Doc # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Text # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Integer # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint () # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Bool # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Char # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Float # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint Int # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint (Bind Var) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint (Expr Var) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint (Elims a) # | |
Defined in Language.Fixpoint.Graph.Deps | |
| PPrint (Bind a) # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint (Cstr a) # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint (Query a) # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint (Var a) # | |
Defined in Language.Fixpoint.Horn.Types | |
| PPrint (Worklist a) # | |
Defined in Language.Fixpoint.Solver.Worklist | |
| (Ord v, Fixpoint v, PPrint v) => PPrint (QualifierV v) # | |
Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualifierV v -> Doc # pprintPrec :: Int -> Tidy -> QualifierV v -> Doc # | |
| Fixpoint a => PPrint (SimpC a) # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Fixpoint a => PPrint (SubC a) # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Fixpoint a => PPrint (WfC a) # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint a => PPrint (SizedEnv a) # | |
Defined in Language.Fixpoint.Types.Environments | |
| Fixpoint a => PPrint (FixResult a) # | |
Defined in Language.Fixpoint.Types.Errors | |
| (PPrint v, Fixpoint v, Ord v) => PPrint (ReftV v) # | |
Defined in Language.Fixpoint.Types.Substitutions | |
| (Ord v, Hashable v, Fixpoint v) => PPrint (SubstV v) # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint a => PPrint (Sol a) # | |
Defined in Language.Fixpoint.Types.Solutions | |
| PPrint a => PPrint (TCEmb a) # | |
Defined in Language.Fixpoint.Types.Sorts | |
| PPrint a => PPrint (Located a) # | |
Defined in Language.Fixpoint.Types.Spans | |
| PPrint a => PPrint (Triggered a) # | |
Defined in Language.Fixpoint.Types.Triggers | |
| Show a => PPrint (Trie a) # | |
Defined in Language.Fixpoint.Utils.Trie | |
| (Show v, PPrint v) => PPrint (PlugTV v) Source # | |
Defined in Language.Haskell.Liquid.Bare.Types | |
| PPrint a => PPrint (Template a) Source # | |
Defined in Language.Haskell.Liquid.Constraint.Template | |
| PPrint ty => PPrint (DataCtorP ty) Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataCtorP ty -> Doc # pprintPrec :: Int -> Tidy -> DataCtorP ty -> Doc # | |
| PPrint (CtxError SpecType) Source # | |
Defined in Language.Haskell.Liquid.UX.Tidy | |
| PPrint (CtxError Doc) Source # | Pretty Printing Error Messages -------------------------------------------- Need to put |
Defined in Language.Haskell.Liquid.UX.Tidy | |
| PPrint (NoReftB b) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint v => PPrint (SizeFunV v) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| PPrint t => PPrint (AREnv t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint a => PPrint (AnnInfo a) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint t => PPrint (Annot t) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| (PPrint v, Ord v, Fixpoint v) => PPrint (BodyV v) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint t => PPrint (CMeasure t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Ord v, Fixpoint v, PPrint v) => PPrint (LMapV v) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| PPrint a => PPrint (Output a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint t => PPrint (RClass t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint t => PPrint (RISig t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| PPrint t => PPrint (RInstance t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (Ord a, PPrint a) => PPrint (HashSet a) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint a => PPrint (Maybe a) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| PPrint a => PPrint [a] # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| (PPrint a, PPrint b) => PPrint (Either a b) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| (Ord b, PPrint b, PPrint a) => PPrint (SEnvB b a) # | |
Defined in Language.Fixpoint.Types.Environments | |
| (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v) => PPrint (ExprBV b v) # | |
Defined in Language.Fixpoint.Types.Refinements | |
| (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => PPrint (KVarSubst b v) # | |
Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVarSubst b v -> Doc # pprintPrec :: Int -> Tidy -> KVarSubst b v -> Doc # | |
| (PPrint e, PPrint t) => PPrint (Bound t e) Source # | |
Defined in Language.Haskell.Liquid.Types.Bounds | |
| (PPrint lname, PPrint ty) => PPrint (DataDeclP lname ty) Source # | |
Defined in Language.Haskell.Liquid.Types.DataDecl Methods pprintTidy :: Tidy -> DataDeclP lname ty -> Doc # pprintPrec :: Int -> Tidy -> DataDeclP lname ty -> Doc # | |
| (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v) => PPrint (PredicateBV b v) Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> PredicateBV b v -> Doc # pprintPrec :: Int -> Tidy -> PredicateBV b v -> Doc # | |
| PPrint v => PPrint (RTVar v s) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| (PPrint r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| (PPrint lname, PPrint ty, PredicateCompat Symbol lname, Fixpoint lname, Ord lname) => PPrint (Spec lname ty) Source # | |
Defined in Language.Haskell.Liquid.Types.Specs Methods pprintTidy :: Tidy -> Spec lname ty -> Doc # pprintPrec :: Int -> Tidy -> Spec lname ty -> Doc # | |
| PPrint t => PPrint (HoleInfo i t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> HoleInfo i t -> Doc # pprintPrec :: Int -> Tidy -> HoleInfo i t -> Doc # | |
| (PPrint t, PPrint a) => PPrint (MSpec t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTAlias tv ty -> Doc # pprintPrec :: Int -> Tidy -> RTAlias tv ty -> Doc # | |
| (PPrint tv, PPrint t) => PPrint (RTEnv tv t) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |
| (Ord a, PPrint a, PPrint b) => PPrint (HashMap a b) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| (PPrint a, PPrint b) => PPrint (a, b) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v) => PPrint (PVarBV b v a) Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods pprintTidy :: Tidy -> PVarBV b v a -> Doc # pprintPrec :: Int -> Tidy -> PVarBV b v a -> Doc # | |
| (PPrint (PredicateBV b v), ToReft (PredicateBV b v), PPrint r, ToReft r) => PPrint (UReftBV b v r) Source # | |
Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> UReftBV b v r -> Doc # pprintPrec :: Int -> Tidy -> UReftBV b v r -> Doc # | |
| (PPrint a, PPrint v, Ord v, Fixpoint v) => PPrint (DefV v t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| (PPrint v, Ord v, Fixpoint v, PPrint t, PPrint a) => PPrint (MeasureV v t a) Source # | |
Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MeasureV v t a -> Doc # pprintPrec :: Int -> Tidy -> MeasureV v t a -> Doc # | |
| (PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) # | |
Defined in Language.Fixpoint.Types.PrettyPrint | |
| (PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) # | |
Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d) -> Doc # | |
| OkRTBV b v c tv r => PPrint (RTypeBV b v c tv r) Source # | Pretty Printing RefType --------------------------------------------------- |
Defined in Language.Haskell.Liquid.Types.PrettyPrint Methods pprintTidy :: Tidy -> RTypeBV b v c tv r -> Doc # pprintPrec :: Int -> Tidy -> RTypeBV b v c tv r -> Doc # | |
| (PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e) # | |
Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> (a, b, c, d, e) -> Doc # pprintPrec :: Int -> Tidy -> (a, b, c, d, e) -> Doc # | |
Modules and Imports
Module Names --------------------------------------------------------------
Constructors
| ModName !ModType !ModuleName |
Instances
| Eq ModName Source # | |||||
| Ord ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Data ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModName -> c ModName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModName # toConstr :: ModName -> Constr # dataTypeOf :: ModName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModName) # gmapT :: (forall b. Data b => b -> b) -> ModName -> ModName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModName -> r # gmapQ :: (forall d. Data d => d -> u) -> ModName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModName -> m ModName # | |||||
| Generic ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show ModName Source # | |||||
| Hashable ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Symbolic ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| PPrint ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Rep ModName Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep ModName = D1 ('MetaData "ModName" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.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 Source # | |||||
| Ord ModType Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Data ModType Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModType -> c ModType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModType # toConstr :: ModType -> Constr # dataTypeOf :: ModType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModType) # gmapT :: (forall b. Data b => b -> b) -> ModType -> ModType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModType -> r # gmapQ :: (forall d. Data d => d -> u) -> ModType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModType -> m ModType # | |||||
| Generic ModType Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show ModType Source # | |||||
| 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.14.1-inplace" 'False) (C1 ('MetaCons "Target" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SrcImport" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpecImport" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
isSrcImport :: ModName -> Bool Source #
isSpecImport :: ModName -> Bool Source #
getModName :: ModName -> ModuleName Source #
getModString :: ModName -> String Source #
Refinement Type Aliases
Refinement Type and Expression Aliases Environment
Constructors
| RTE | |
Fields
| |
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 Methods mempty :: Diagnostics # mappend :: Diagnostics -> Diagnostics -> Diagnostics # mconcat :: [Diagnostics] -> Diagnostics # | |
| Semigroup Diagnostics Source # | |
Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: Diagnostics -> Diagnostics -> Diagnostics # sconcat :: NonEmpty Diagnostics -> Diagnostics # stimes :: Integral b => b -> Diagnostics -> Diagnostics # | |
| Eq Diagnostics Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
mkDiagnostics :: [Warning] -> [Error] -> Diagnostics Source #
noErrors :: Diagnostics -> Bool Source #
allWarnings :: Diagnostics -> [Warning] Source #
allErrors :: Diagnostics -> [Error] Source #
printWarning :: Logger -> Warning -> IO () Source #
Printing Warnings ---------------------------------------------------------
Source information (associated with constraints)
Source Information Associated With Constraints ----------------------------
Instances
| NFData Cinfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Eq Cinfo Source # | |||||
| Generic Cinfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show 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.14.1-inplace" 'False) (C1 ('MetaCons "Ci" 'PrefixI 'True) (S1 ('MetaSel ('Just "ci_loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ci_err") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Error)) :*: S1 ('MetaSel ('Just "ci_var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Var))))) | |||||
Measures
data MeasureV v ty ctor Source #
Constructors
| M | |
Fields
| |
Instances
| Expand BareMeasure Source # | |||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source # | |||||
| Bifunctor (MeasureV v) Source # | |||||
| Functor (MeasureV v ty) Source # | |||||
| Subable (Measure ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
Methods syms :: Measure ty ctor -> [Variable (Measure ty ctor)] substa :: (Variable (Measure ty ctor) -> Variable (Measure ty ctor)) -> Measure ty ctor -> Measure ty ctor substf :: (Variable (Measure ty ctor) -> ExprBV (Variable (Measure ty ctor)) (Variable (Measure ty ctor))) -> Measure ty ctor -> Measure ty ctor subst :: SubstV (Variable (Measure ty ctor)) -> Measure ty ctor -> Measure ty ctor subst1 :: Measure ty ctor -> (Variable (Measure ty ctor), ExprBV (Variable (Measure ty ctor)) (Variable (Measure ty ctor))) -> Measure ty ctor | |||||
| Loc (Measure a b) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (Binary v, Binary ctor, Binary ty) => Binary (MeasureV v ty ctor) Source # | |||||
| (Eq ctor, Eq ty, Eq v) => Eq (MeasureV v ty ctor) Source # | |||||
| (Data ctor, Data ty, Data v) => Data (MeasureV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MeasureV v ty ctor -> c (MeasureV v ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MeasureV v ty ctor) # toConstr :: MeasureV v ty ctor -> Constr # dataTypeOf :: MeasureV v ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MeasureV v ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MeasureV v ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> MeasureV v ty ctor -> MeasureV v ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MeasureV v ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MeasureV v ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> MeasureV v ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MeasureV v ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureV v ty ctor -> m (MeasureV v ty ctor) # | |||||
| Generic (MeasureV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| PPrint (MeasureV v t a) => Show (MeasureV v t a) Source # | |||||
| (Hashable ctor, Hashable ty, Hashable v) => Hashable (MeasureV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (PPrint v, Ord v, Fixpoint v, PPrint t, PPrint a) => PPrint (MeasureV v t a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MeasureV v t a -> Doc # pprintPrec :: Int -> Tidy -> MeasureV v t a -> Doc # | |||||
| type Variable (Measure ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Variable (Measure ty ctor) = Symbol | |||||
| type Rep (MeasureV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (MeasureV v ty ctor) = D1 ('MetaData "MeasureV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "M" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "msSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty)) :*: (S1 ('MetaSel ('Just "msEqns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefV v ty ctor]) :*: (S1 ('MetaSel ('Just "msKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 MeasureKind) :*: S1 ('MetaSel ('Just "msUnSorted") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UnSortedExprs))))) | |||||
type UnSortedExprs = [UnSortedExpr] Source #
type UnSortedExpr = ([Symbol], Expr) Source #
data MeasureKind Source #
Constructors
| MsReflect | due to `reflect foo`, used for opaque reflection |
| MsMeasure | due to `measure foo` with old-style (non-haskell) equations |
| MsLifted | due to `measure foo` with new-style haskell equations |
| MsClass | due to `class measure` definition |
| MsAbsMeasure | due to `measure foo` without equations c.f. testsposT1223.hs |
| MsSelector | due to selector-fields e.g. `data Foo = Foo { fld :: Int }` |
| MsChecker | due to checkers e.g. `is-F` for `data Foo = F ... | G ...` |
Instances
| Binary MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Eq MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Ord MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods compare :: MeasureKind -> MeasureKind -> Ordering # (<) :: MeasureKind -> MeasureKind -> Bool # (<=) :: MeasureKind -> MeasureKind -> Bool # (>) :: MeasureKind -> MeasureKind -> Bool # (>=) :: MeasureKind -> MeasureKind -> Bool # max :: MeasureKind -> MeasureKind -> MeasureKind # min :: MeasureKind -> MeasureKind -> MeasureKind # | |||||
| Data MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MeasureKind -> c MeasureKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MeasureKind # toConstr :: MeasureKind -> Constr # dataTypeOf :: MeasureKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MeasureKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MeasureKind) # gmapT :: (forall b. Data b => b -> b) -> MeasureKind -> MeasureKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MeasureKind -> r # gmapQ :: (forall d. Data d => d -> u) -> MeasureKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MeasureKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MeasureKind -> m MeasureKind # | |||||
| Generic MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MeasureKind -> ShowS # show :: MeasureKind -> String # showList :: [MeasureKind] -> ShowS # | |||||
| Hashable MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Rep MeasureKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep MeasureKind = D1 ('MetaData "MeasureKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) ((C1 ('MetaCons "MsReflect" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MsMeasure" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsLifted" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MsClass" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsAbsMeasure" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "MsSelector" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MsChecker" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
Instances
| Functor CMeasure Source # | |||||
| Data ty => Data (CMeasure ty) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMeasure ty -> c (CMeasure ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CMeasure ty) # toConstr :: CMeasure ty -> Constr # dataTypeOf :: CMeasure ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CMeasure ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CMeasure ty)) # gmapT :: (forall b. Data b => b -> b) -> CMeasure ty -> CMeasure ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMeasure ty -> r # gmapQ :: (forall d. Data d => d -> u) -> CMeasure ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CMeasure ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMeasure ty -> m (CMeasure ty) # | |||||
| Generic (CMeasure ty) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| 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.14.1-inplace" 'False) (C1 ('MetaCons "CM" 'PrefixI 'True) (S1 ('MetaSel ('Just "cName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "cSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ty))) | |||||
Constructors
| Def | |
Instances
| Expand BareDef Source # | |||||
| Bifunctor (DefV v) Source # | |||||
| Functor (DefV v ty) Source # | |||||
| Subable (Def ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
Methods syms :: Def ty ctor -> [Variable (Def ty ctor)] substa :: (Variable (Def ty ctor) -> Variable (Def ty ctor)) -> Def ty ctor -> Def ty ctor substf :: (Variable (Def ty ctor) -> ExprBV (Variable (Def ty ctor)) (Variable (Def ty ctor))) -> Def ty ctor -> Def ty ctor subst :: SubstV (Variable (Def ty ctor)) -> Def ty ctor -> Def ty ctor subst1 :: Def ty ctor -> (Variable (Def ty ctor), ExprBV (Variable (Def ty ctor)) (Variable (Def ty ctor))) -> Def ty ctor | |||||
| (Binary ty, Binary v, Binary ctor) => Binary (DefV v ty ctor) Source # | |||||
| (Eq ctor, Eq ty, Eq v) => Eq (DefV v ty ctor) Source # | |||||
| (Data ctor, Data ty, Data v) => Data (DefV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefV v ty ctor -> c (DefV v ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefV v ty ctor) # toConstr :: DefV v ty ctor -> Constr # dataTypeOf :: DefV v ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (DefV v ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefV v ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> DefV v ty ctor -> DefV v ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefV v ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefV v ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> DefV v ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DefV v ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefV v ty ctor -> m (DefV v ty ctor) # | |||||
| Generic (DefV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (Show ctor, Show ty, Show v, Ord v, Fixpoint v) => Show (DefV v ty ctor) Source # | |||||
| (Hashable ctor, Hashable ty, Hashable v) => Hashable (DefV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (PPrint a, PPrint v, Ord v, Fixpoint v) => PPrint (DefV v t a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Variable (Def ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Variable (Def ty ctor) = Symbol | |||||
| type Rep (DefV v ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (DefV v ty ctor) = D1 ('MetaData "DefV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) ((S1 ('MetaSel ('Just "measure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located LHName)) :*: S1 ('MetaSel ('Just "ctor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ctor)) :*: (S1 ('MetaSel ('Just "dsort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ty)) :*: (S1 ('MetaSel ('Just "binds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Maybe ty)]) :*: S1 ('MetaSel ('Just "body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BodyV v)))))) | |||||
Constructors
| E (ExprV v) | Measure Refinement: {v | v = e } |
| P (ExprV v) | Measure Refinement: {v | (? v) = p } |
| R Symbol (ExprV v) | Measure Refinement: {v | p} |
Instances
| Functor BodyV Source # | |||||
| Foldable BodyV Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => BodyV m -> m # foldMap :: Monoid m => (a -> m) -> BodyV a -> m # foldMap' :: Monoid m => (a -> m) -> BodyV a -> m # foldr :: (a -> b -> b) -> b -> BodyV a -> b # foldr' :: (a -> b -> b) -> b -> BodyV a -> b # foldl :: (b -> a -> b) -> b -> BodyV a -> b # foldl' :: (b -> a -> b) -> b -> BodyV a -> b # foldr1 :: (a -> a -> a) -> BodyV a -> a # foldl1 :: (a -> a -> a) -> BodyV a -> a # elem :: Eq a => a -> BodyV a -> Bool # maximum :: Ord a => BodyV a -> a # minimum :: Ord a => BodyV a -> a # | |||||
| Traversable BodyV Source # | |||||
| Subable Body Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
Methods syms :: Body -> [Variable Body] substa :: (Variable Body -> Variable Body) -> Body -> Body substf :: (Variable Body -> ExprBV (Variable Body) (Variable Body)) -> Body -> Body subst :: SubstV (Variable Body) -> Body -> Body subst1 :: Body -> (Variable Body, ExprBV (Variable Body) (Variable Body)) -> Body | |||||
| Expand Body Source # | |||||
| Binary v => Binary (BodyV v) Source # | |||||
| Eq v => Eq (BodyV v) Source # | |||||
| Data v => Data (BodyV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BodyV v -> c (BodyV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BodyV v) # toConstr :: BodyV v -> Constr # dataTypeOf :: BodyV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BodyV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BodyV v)) # gmapT :: (forall b. Data b => b -> b) -> BodyV v -> BodyV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BodyV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BodyV v -> r # gmapQ :: (forall d. Data d => d -> u) -> BodyV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BodyV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BodyV v -> m (BodyV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BodyV v -> m (BodyV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BodyV v -> m (BodyV v) # | |||||
| Generic (BodyV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (Show v, Ord v, Fixpoint v) => Show (BodyV v) Source # | |||||
| Hashable v => Hashable (BodyV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (PPrint v, Ord v, Fixpoint v) => PPrint (BodyV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Variable Body Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Variable Body = Symbol | |||||
| type Rep (BodyV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (BodyV v) = D1 ('MetaData "BodyV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "E" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "P" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))) :+: C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))))) | |||||
Constructors
| MSpec | |
Instances
| Bifunctor MSpec Source # | |||||
| Functor (MSpec ty) Source # | |||||
| Eq ctor => Monoid (MSpec ty ctor) Source # | |||||
| Eq ctor => Semigroup (MSpec ty ctor) Source # | |||||
| (Data ctor, Data ty) => Data (MSpec ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) # toConstr :: MSpec ty ctor -> Constr # dataTypeOf :: MSpec ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # | |||||
| Generic (MSpec ty ctor) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (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 type Rep (MSpec ty ctor) = D1 ('MetaData "MSpec" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "MSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctorMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LHName [Def ty ctor])) :*: S1 ('MetaSel ('Just "measMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ctor)))) :*: (S1 ('MetaSel ('Just "cmeasMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap (Located LHName) (Measure ty ()))) :*: S1 ('MetaSel ('Just "imeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ctor])))) | |||||
mapMeasureTy :: (ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor Source #
emapDefM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> DefV v0 ty0 ctor -> m (DefV v1 ty1 ctor) Source #
mapMeasureV :: (v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor Source #
emapMeasureM :: Monad m => ([Symbol] -> v0 -> m v1) -> ([Symbol] -> ty0 -> m ty1) -> MeasureV v0 ty0 ctor -> m (MeasureV v1 ty1 ctor) Source #
Type Classes
Constructors
| RClass | |
Instances
| Functor RClass Source # | |||||
| Foldable RClass Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => RClass m -> m # foldMap :: Monoid m => (a -> m) -> RClass a -> m # foldMap' :: Monoid m => (a -> m) -> RClass a -> m # foldr :: (a -> b -> b) -> b -> RClass a -> b # foldr' :: (a -> b -> b) -> b -> RClass a -> b # foldl :: (b -> a -> b) -> b -> RClass a -> b # foldl' :: (b -> a -> b) -> b -> RClass a -> b # foldr1 :: (a -> a -> a) -> RClass a -> a # foldl1 :: (a -> a -> a) -> RClass a -> a # elem :: Eq a => a -> RClass a -> Bool # maximum :: Ord a => RClass a -> a # minimum :: Ord a => RClass a -> a # | |||||
| Traversable RClass Source # | |||||
| Binary ty => Binary (RClass ty) Source # | |||||
| Eq ty => Eq (RClass ty) Source # | |||||
| Data ty => Data (RClass ty) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RClass ty -> c (RClass ty) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RClass ty) # toConstr :: RClass ty -> Constr # dataTypeOf :: RClass ty -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RClass ty)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RClass ty)) # gmapT :: (forall b. Data b => b -> b) -> RClass ty -> RClass ty # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RClass ty -> r # gmapQ :: (forall d. Data d => d -> u) -> RClass ty -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RClass ty -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RClass ty -> m (RClass ty) # | |||||
| Generic (RClass ty) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show ty => Show (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.14.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 [(Located LHName, 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 | |
| ProjectE | Projecting out field of |
Instances
| NFData KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Eq KVKind Source # | |||||
| Ord KVKind Source # | |||||
| Data KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVKind -> c KVKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVKind # toConstr :: KVKind -> Constr # dataTypeOf :: KVKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVKind) # gmapT :: (forall b. Data b => b -> b) -> KVKind -> KVKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVKind -> r # gmapQ :: (forall d. Data d => d -> u) -> KVKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KVKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVKind -> m KVKind # | |||||
| Generic KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show KVKind Source # | |||||
| Hashable KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| PPrint KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Rep KVKind Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep KVKind = D1 ('MetaData "KVKind" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.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 "ProjectE" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
Instances
| NFData KVProf Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Generic KVProf Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| PPrint KVProf Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| type Rep KVProf Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
emptyKVProf :: KVProf Source #
Misc
mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty Source #
A map over a RTAlias type parameters.
CoreToLogic
Constructors
| LM | |
toLogicMap :: [(LocSymbol, ([Symbol], Expr))] -> LogicMap Source #
eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr Source #
Instances
| Functor LMapV Source # | |||||
| Binary v => Binary (LMapV v) Source # | |||||
| Eq v => Eq (LMapV v) Source # | |||||
| Data v => Data (LMapV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LMapV v -> c (LMapV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LMapV v) # toConstr :: LMapV v -> Constr # dataTypeOf :: LMapV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LMapV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LMapV v)) # gmapT :: (forall b. Data b => b -> b) -> LMapV v -> LMapV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LMapV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LMapV v -> r # gmapQ :: (forall d. Data d => d -> u) -> LMapV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LMapV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LMapV v -> m (LMapV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LMapV v -> m (LMapV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LMapV v -> m (LMapV v) # | |||||
| Generic (LMapV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| (Show v, Ord v, Fixpoint v) => Show (LMapV v) Source # | |||||
| Hashable v => Hashable (LMapV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| (Ord v, Fixpoint v, PPrint v) => PPrint (LMapV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.PrettyPrint | |||||
| type Rep (LMapV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types type Rep (LMapV v) = D1 ('MetaData "LMapV" "Language.Haskell.Liquid.Types.Types" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocSymbol) :*: (S1 ('MetaSel ('Just "lmArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "lmExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ExprV v))))) | |||||
Refined Instances
Refined Instances ---------------------------------------------------------
Constructors
| RI | |
Instances
| Functor RInstance Source # | |||||
| Foldable RInstance Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => RInstance m -> m # foldMap :: Monoid m => (a -> m) -> RInstance a -> m # foldMap' :: Monoid m => (a -> m) -> RInstance a -> m # foldr :: (a -> b -> b) -> b -> RInstance a -> b # foldr' :: (a -> b -> b) -> b -> RInstance a -> b # foldl :: (b -> a -> b) -> b -> RInstance a -> b # foldl' :: (b -> a -> b) -> b -> RInstance a -> b # foldr1 :: (a -> a -> a) -> RInstance a -> a # foldl1 :: (a -> a -> a) -> RInstance a -> a # toList :: RInstance a -> [a] # length :: RInstance a -> Int # elem :: Eq a => a -> RInstance a -> Bool # maximum :: Ord a => RInstance a -> a # minimum :: Ord a => RInstance a -> a # | |||||
| Traversable RInstance Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types | |||||
| Binary t => Binary (RInstance t) Source # | |||||
| Eq t => Eq (RInstance t) Source # | |||||
| Data t => Data (RInstance t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RInstance t -> c (RInstance t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RInstance t) # toConstr :: RInstance t -> Constr # dataTypeOf :: RInstance t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RInstance t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RInstance t)) # gmapT :: (forall b. Data b => b -> b) -> RInstance t -> RInstance t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RInstance t -> r # gmapQ :: (forall d. Data d => d -> u) -> RInstance t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RInstance t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RInstance t -> m (RInstance t) # | |||||
| Generic (RInstance t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show t => Show (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.14.1-inplace" 'False) (C1 ('MetaCons "RI" 'PrefixI 'True) ((S1 ('MetaSel ('Just "riclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BTyCon) :*: S1 ('MetaSel ('Just "riDictName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located LHName)))) :*: (S1 ('MetaSel ('Just "ritype") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "risigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Located LHName, RISig t)])))) | |||||
Instances
| Functor RISig Source # | |||||
| Foldable RISig Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods fold :: Monoid m => RISig m -> m # foldMap :: Monoid m => (a -> m) -> RISig a -> m # foldMap' :: Monoid m => (a -> m) -> RISig a -> m # foldr :: (a -> b -> b) -> b -> RISig a -> b # foldr' :: (a -> b -> b) -> b -> RISig a -> b # foldl :: (b -> a -> b) -> b -> RISig a -> b # foldl' :: (b -> a -> b) -> b -> RISig a -> b # foldr1 :: (a -> a -> a) -> RISig a -> a # foldl1 :: (a -> a -> a) -> RISig a -> a # elem :: Eq a => a -> RISig a -> Bool # maximum :: Ord a => RISig a -> a # minimum :: Ord a => RISig a -> a # | |||||
| Traversable RISig Source # | |||||
| Binary t => Binary (RISig t) Source # | |||||
| Eq t => Eq (RISig t) Source # | |||||
| Data t => Data (RISig t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RISig t -> c (RISig t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RISig t) # toConstr :: RISig t -> Constr # dataTypeOf :: RISig t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RISig t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RISig t)) # gmapT :: (forall b. Data b => b -> b) -> RISig t -> RISig t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RISig t -> r # gmapQ :: (forall d. Data d => d -> u) -> RISig t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RISig t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RISig t -> m (RISig t) # | |||||
| Generic (RISig t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.Types Associated Types
| |||||
| Show t => Show (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.14.1-inplace" 'False) (C1 ('MetaCons "RIAssumed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "RISig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) | |||||
data MethodType t Source #
Constructors
| MT | |
Fields
| |
Instances
| Show t => Show (MethodType t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MethodType t -> ShowS # show :: MethodType t -> String # showList :: [MethodType t] -> ShowS # | |
getMethodType :: MethodType t -> Maybe t Source #
String Literals
liquidBegin :: String Source #
Values Related to Specifications ------------------------------------
Constructors
| Axiom | |
Orphan instances
| NFData CoreExpr Source # | |||||
| Ord DataCon Source # | |||||
| Ord TyCon Source # | |||||
| Symbolic DataCon Source # | |||||
| Symbolic ModuleName Source # | |||||
Methods symbol :: ModuleName -> Symbol | |||||
| PPrint TyThing Source # | |||||
| NFData a => NFData (TError a) Source # | |||||
| Subable t => Subable (WithModel t) Source # | |||||
Associated Types
Methods syms :: WithModel t -> [Variable (WithModel t)] substa :: (Variable (WithModel t) -> Variable (WithModel t)) -> WithModel t -> WithModel t substf :: (Variable (WithModel t) -> ExprBV (Variable (WithModel t)) (Variable (WithModel t))) -> WithModel t -> WithModel t subst :: SubstV (Variable (WithModel t)) -> WithModel t -> WithModel t subst1 :: WithModel t -> (Variable (WithModel t), ExprBV (Variable (WithModel t)) (Variable (WithModel t))) -> WithModel t | |||||