| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.RType
Contents
- Bare Type Constructors and Variables
- Refined Type Constructors
- Refinement Types
- Classes describing operations on
RTypes - Type Variables
- Predicate Variables
- Expression Arguments
- Manipulating
Predicates - Refinements
- Parse-time entities describing refined data types
- Pre-instantiated RType
- Instantiated RType
- Printer Configuration
- Refined Function Info
- Converting to and from refinements
- Orphan instances
Description
This module contains the types to represent refinement types.
Synopsis
- data BTyCon = BTyCon {}
- mkBTyCon :: Located LHName -> BTyCon
- isClassBTyCon :: BTyCon -> Bool
- newtype BTyVar = BTV LocSymbol
- data RTyCon = RTyCon TyCon ![RPVar] !TyConInfo
- data TyConInfo = TyConInfo {}
- defaultTyConInfo :: TyConInfo
- rTyConPVs :: RTyCon -> [RPVar]
- isClassType :: TyConable c => RTypeV v c t t1 -> Bool
- isEqType :: TyConable c => RTypeV v c t t1 -> Bool
- isRVar :: RType c tv r -> Bool
- isBool :: RType RTyCon t t1 -> Bool
- isEmbeddedClass :: TyConable c => RTypeV v c t t1 -> Bool
- type RType c tv r = RTypeV Symbol c tv r
- type RTypeV v c tv = RTypeBV Symbol v c tv
- data RTypeBV b v c tv r
- type Ref τ t = RefB Symbol τ t
- data RefB b τ t = RProp {}
- type RTProp c tv r = RTPropV Symbol c tv r
- type RTPropV v c tv r = RTPropBV Symbol v c tv r
- type RTPropBV b v c tv r = RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)
- rPropP :: [(b, τ)] -> r -> RefB b τ (RTypeV v c tv r)
- newtype RTyVar = RTV TyVar
- type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, PPrint (ReftVar r), Fixpoint (ReftVar r), ToReft r, ReftBind r ~ Symbol, Eq c, Eq tv, Ord (ReftVar r), Hashable tv)
- type OkRTBV b v c tv r = (TyConable c, PPrint b, PPrint v, PPrint tv, PPrint c, PPrint r, PPrint (ReftVar r), Fixpoint b, Fixpoint v, Fixpoint (ReftVar r), Binder b, ToReft r, ReftBind r ~ b, Eq c, Eq tv, Ord b, Ord v, Ord (ReftVar r), Hashable tv)
- class Eq c => TyConable c where
- 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
- type PVar t = PVarV Symbol t
- type PVarV v t = PVarBV Symbol v t
- data PVarBV b v t = PV {}
- pvType :: PVarBV b v t -> t
- type Predicate = PredicateV Symbol
- type PredicateV v = PredicateBV Symbol v
- newtype PredicateBV b v = Pr [UsedPVarBV b v]
- class PredicateCompat b v where
- notExprArg :: RTypeV v c tv r -> Bool
- emapExprVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v')
- mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v'
- emapPredicateVM :: Monad m => ([Symbol] -> v -> m v') -> PredicateV v -> m (PredicateV v')
- mapPVarV :: (v -> v') -> (t -> t') -> PVarBV b v t -> PVarBV b v' t'
- emapPVarVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t')
- emapSubstVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> KVarSubst b v -> m (KVarSubst b v')
- pvars :: PredicateBV b v -> [UsedPVarBV b v]
- pApp :: PredicateCompat b v => v -> [ExprBV b v] -> ExprBV b v
- type UReft r = UReftV Symbol r
- type UReftV v r = UReftBV Symbol v r
- data UReftBV b v r = MkUReft {
- ur_reft :: !r
- ur_pred :: !(PredicateBV b v)
- mapUReftV :: (v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
- emapUReftVM :: Monad m => ([Symbol] -> v -> m v') -> (r -> m r') -> UReftV v r -> m (UReftV v' r')
- type NoReft = NoReftB Symbol
- data NoReftB b = NoReft
- type SizeFun = SizeFunV Symbol
- data SizeFunV v
- = IdSizeFun
- | SymSizeFun (Located v)
- szFun :: SizeFun -> Symbol -> Expr
- data TyConP = TyConP {
- tcpLoc :: !SourcePos
- tcpCon :: !TyCon
- tcpFreeTyVarsTy :: ![RTyVar]
- tcpFreePredTy :: ![PVar RSort]
- tcpVarianceTs :: !VarianceInfo
- tcpVariancePs :: !VarianceInfo
- tcpSizeFun :: !(Maybe SizeFun)
- type RRType = RTypeV Symbol RTyCon RTyVar
- type RRProp r = Ref RSort (RRType r)
- type BRType = RTypeV Symbol BTyCon BTyVar
- type BRProp r = BRPropV Symbol r
- type BRPropV v r = Ref (BSortV v) (BRTypeV v r)
- type BSort = BRType NoReft
- type BSortV v = BRTypeV v NoReft
- type BPVar = PVar BSort
- type RTVU c tv = RTVUV Symbol c tv
- type PVU c tv = PVUV Symbol c tv
- type BareType = BareTypeV Symbol
- type BareTypeLHName = BareTypeV LHName
- type BareTypeParsed = BareTypeV LocSymbol
- type BareTypeV v = BRTypeV v (RReftV v)
- type SpecType = RRType RReft
- type SpecProp = RRProp RReft
- type SpecRTVar = RTVar RTyVar RSort
- type LocBareType = Located BareType
- type LocBareTypeLHName = Located BareTypeLHName
- type LocBareTypeParsed = Located BareTypeParsed
- type LocSpecType = Located SpecType
- type RSort = RRType NoReft
- type UsedPVar = UsedPVarV Symbol
- type UsedPVarV v = UsedPVarBV Symbol v
- type RPVar = PVar RSort
- type RReft = RReftV Symbol
- type RReftV v = RReftBV Symbol v
- type RReftBV b v = UReftBV b v (ReftBV b v)
- data PPEnv = PP {}
- ppEnv :: PPEnv
- ppEnvShort :: PPEnv -> PPEnv
- newtype RFInfo = RFInfo {}
- defRFInfo :: RFInfo
- mkRFInfo :: Config -> RFInfo
- classRFInfo :: Bool -> RFInfo
- class (Binder (ReftBind r), Eq (ReftVar r)) => ToReft r where
- class Semigroup r => Meet r where
- meet :: r -> r -> r
- class Top r where
- top :: r -> r
- class (ToReft r, Meet r, Top r) => IsReft r where
- isTauto :: ToReft r => r -> Bool
- trueReft :: IsReft r => r
Bare Type Constructors and Variables
Constructors
| BTyCon | |
Instances
isClassBTyCon :: BTyCon -> Bool Source #
Instances
| Binary BTyVar Source # | |||||
| NFData BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq BTyVar Source # | |||||
| Ord DataDecl Source # | |||||
Defined in Language.Haskell.Liquid.Types.DataDecl | |||||
| Ord BTyVar Source # | |||||
| Data BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BTyVar -> c BTyVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BTyVar # toConstr :: BTyVar -> Constr # dataTypeOf :: BTyVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BTyVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BTyVar) # gmapT :: (forall b. Data b => b -> b) -> BTyVar -> BTyVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BTyVar -> r # gmapQ :: (forall d. Data d => d -> u) -> BTyVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BTyVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BTyVar -> m BTyVar # | |||||
| Generic BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show BTyVar Source # | |||||
| Show BareSpec Source # | |||||
| Hashable BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Symbolic BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| PPrint BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Expand DataCtor Source # | |||||
| Expand DataDecl Source # | |||||
| Expand BareType Source # |
| ||||
| Expand BareDef Source # | |||||
| Expand BareMeasure Source # | |||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source # | |||||
| Expand BareSpec Source # | |||||
| Expand BareRTAlias Source # | |||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source # | |||||
| CompatibleBinder Symbol BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods coerceBinder :: BTyVar -> Symbol Source # | |||||
| FreeVar BTyCon BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||
| SubsTy BTyVar BSort BSort Source # | |||||
| SubsTy BTyVar BSort BTyCon Source # | |||||
| SubsTy Symbol Symbol (BRType r) Source # | |||||
| SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # | |||||
| SubsTy BTyVar (RType BTyCon BTyVar NoReft) Sort Source # | |||||
| SubsTy BTyVar (RType c BTyVar NoReft) BTyVar Source # | |||||
| SubsTy BTyVar (RType c BTyVar NoReft) (RTVar BTyVar (RType c BTyVar NoReft)) Source # | |||||
| Expand (BRType NoReft) Source # | |||||
| CompatibleBinder (Located Symbol) BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods coerceBinder :: BTyVar -> Located Symbol Source # | |||||
| Meet (RTProp BTyCon BTyVar NoReft) Source # | |||||
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |||||
| Meet (RType BTyCon BTyVar (UReft Reft)) Source # | |||||
| type Rep BTyVar Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
Refined Type Constructors
Instances
| NFData RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| NFData REnv Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.Types | |||||||||
| Monoid REnv Source # | |||||||||
| Semigroup REnv Source # | |||||||||
| Eq RTyCon Source # | |||||||||
| Data RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyCon -> c RTyCon # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyCon # toConstr :: RTyCon -> Constr # dataTypeOf :: RTyCon -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyCon) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyCon) # gmapT :: (forall b. Data b => b -> b) -> RTyCon -> RTyCon # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyCon -> r # gmapQ :: (forall d. Data d => d -> u) -> RTyCon -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyCon -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyCon -> m RTyCon # | |||||||||
| Exception Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String # backtraceDesired :: Error -> Bool # | |||||||||
| Generic RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Show RTyCon Source # | |||||||||
| Show Error Source # | |||||||||
| Hashable RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| Symbolic RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Fixpoint RTyCon Source # | |||||||||
| PPrint RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| PPrint Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Expand SpecType Source # |
| ||||||||
| REq SpecType 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 # | |||||||||
| Result Error Source # | |||||||||
| FreeVar RTyCon RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| SubsTy TyVar Type SpecType Source # | |||||||||
| SubsTy Symbol RSort Sort Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| 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 # | |||||||||
| (Freshable m Integer, Freshable m r, IsReft r, Subable r, Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => Freshable m (RRType r) Source # | |||||||||
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) RTyVar Source # | |||||||||
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) (RTVar RTyVar (RType RTyCon RTyVar NoReft)) Source # | |||||||||
| Exception [Error] Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String # backtraceDesired :: [Error] -> Bool # | |||||||||
| PPrint (CtxError SpecType) Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- | ||||||||
Defined in Language.Haskell.Liquid.Types.RefType Associated Types
Methods syms :: RRProp Reft -> [Variable (RRProp Reft)] substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft | |||||||||
| Result [Error] Source # | |||||||||
| Meet (RTProp RTyCon RTyVar Reft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| Semigroup (RType RTyCon RTyVar r) => Meet (RType RTyCon RTyVar r) Source # | |||||||||
| type Rep RTyCon Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Rep RTyCon = D1 ('MetaData "RTyCon" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "RTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtc_tc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyCon) :*: (S1 ('MetaSel ('Just "rtc_pvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RPVar]) :*: S1 ('MetaSel ('Just "rtc_info") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyConInfo)))) | |||||||||
| type Variable (RRProp Reft) | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType type Variable (RRProp Reft) = Symbol | |||||||||
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
| NFData TyConInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Data TyConInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType 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 # | |||||
| Generic TyConInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show TyConInfo Source # | |||||
| type Rep TyConInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep TyConInfo = D1 ('MetaData "TyConInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.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))))) | |||||
Refinement Types
data RTypeBV b v c tv r Source #
Constructors
| RVar | |
| RFun | |
| RAllT | |
| RAllP | "forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ (rt_pvbind) |
| RApp | For example, in [a]- v > h}>, we apply (via |
| RAllE | |
| REx | |
| RExprArg (Located (ExprBV b v)) | 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
| NFData REnv Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.Types | |||||||||
| Monoid REnv Source # | |||||||||
| Semigroup REnv Source # | |||||||||
| Ord DataDecl Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.DataDecl | |||||||||
| Exception Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String # backtraceDesired :: Error -> Bool # | |||||||||
| Show BareSpec Source # | |||||||||
| Show Error Source # | |||||||||
| PPrint Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Expand DataCtor Source # | |||||||||
| Expand DataDecl Source # | |||||||||
| Expand BareType Source # |
| ||||||||
| Expand SpecType Source # |
| ||||||||
| Expand BareDef Source # | |||||||||
| Expand BareMeasure Source # | |||||||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source # | |||||||||
| Expand BareSpec Source # | |||||||||
| Expand BareRTAlias Source # | |||||||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source # | |||||||||
| REq SpecType Source # | |||||||||
| Result Error Source # | |||||||||
| 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 Symbol Symbol (BRType r) Source # | |||||||||
| SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # | |||||||||
| (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv NoReft)) => SubsTy tv ty (RTProp c tv (UReft r)) Source # | |||||||||
| (Freshable m Integer, Freshable m r, IsReft r, Subable r, Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => Freshable m (RRType 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 # | |||||||||
| Exception [Error] Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String # backtraceDesired :: [Error] -> Bool # | |||||||||
| PPrint (CtxError SpecType) Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- | ||||||||
Defined in Language.Haskell.Liquid.Types.RefType Associated Types
Methods syms :: RRProp Reft -> [Variable (RRProp Reft)] substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft | |||||||||
| Expand (BRType NoReft) Source # | |||||||||
| Result [Error] Source # | |||||||||
| Show tv => Show (RTVU c tv) Source # | |||||||||
| (PPrint r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| (NFData c, NFData tv, NFData r) => NFData (RType c tv r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| (Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c) => Eq (RType c tv NoReft) Source # | |||||||||
| PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # | |||||||||
| PPrint (RType c tv r) => Show (RType c tv r) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar NoReft) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar Reft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| Meet (RType BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| Semigroup (RType RTyCon RTyVar r) => Meet (RType RTyCon RTyVar r) Source # | |||||||||
| Functor (RTypeBV b v c tv) Source # | |||||||||
| Foldable (RTypeBV b v c tv) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => RTypeBV b v c tv m -> m # foldMap :: Monoid m => (a -> m) -> RTypeBV b v c tv a -> m # foldMap' :: Monoid m => (a -> m) -> RTypeBV b v c tv a -> m # foldr :: (a -> b0 -> b0) -> b0 -> RTypeBV b v c tv a -> b0 # foldr' :: (a -> b0 -> b0) -> b0 -> RTypeBV b v c tv a -> b0 # foldl :: (b0 -> a -> b0) -> b0 -> RTypeBV b v c tv a -> b0 # foldl' :: (b0 -> a -> b0) -> b0 -> RTypeBV b v c tv a -> b0 # foldr1 :: (a -> a -> a) -> RTypeBV b v c tv a -> a # foldl1 :: (a -> a -> a) -> RTypeBV b v c tv a -> a # toList :: RTypeBV b v c tv a -> [a] # null :: RTypeBV b v c tv a -> Bool # length :: RTypeBV b v c tv a -> Int # elem :: Eq a => a -> RTypeBV b v c tv a -> Bool # maximum :: Ord a => RTypeBV b v c tv a -> a # minimum :: Ord a => RTypeBV b v c tv a -> a # | |||||||||
| Traversable (RTypeBV b v c tv) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods traverse :: Applicative f => (a -> f b0) -> RTypeBV b v c tv a -> f (RTypeBV b v c tv b0) # sequenceA :: Applicative f => RTypeBV b v c tv (f a) -> f (RTypeBV b v c tv a) # mapM :: Monad m => (a -> m b0) -> RTypeBV b v c tv a -> m (RTypeBV b v c tv b0) # sequence :: Monad m => RTypeBV b v c tv (m a) -> m (RTypeBV b v c tv a) # | |||||||||
| (Binary v, Binary tv, Binary r, Binary b, Binary c) => Binary (RTypeBV b v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTPropBV v v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, FreeVar c tv, Subable r, Variable r ~ v, ReftBind r ~ v, IsReft r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTypeBV v v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTPropBV v v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, FreeVar c tv, Subable r, Variable r ~ v, ReftBind r ~ v, IsReft r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTypeBV v v c tv r) Source # | |||||||||
| (Eq tv, Eq c, Eq v, Eq b, Eq r) => Eq (RTypeBV b v c tv r) Source # | |||||||||
| (Data tv, Data c, Data v, Data b, Data r) => Data (RTypeBV b v c tv r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c0 (d -> b0) -> d -> c0 b0) -> (forall g. g -> c0 g) -> RTypeBV b v c tv r -> c0 (RTypeBV b v c tv r) # gunfold :: (forall b0 r0. Data b0 => c0 (b0 -> r0) -> c0 r0) -> (forall r1. r1 -> c0 r1) -> Constr -> c0 (RTypeBV b v c tv r) # toConstr :: RTypeBV b v c tv r -> Constr # dataTypeOf :: RTypeBV b v c tv r -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (RTypeBV b v c tv r)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (RTypeBV b v c tv r)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> RTypeBV b v c tv r -> RTypeBV b v c tv r # gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> RTypeBV b v c tv r -> r0 # gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> RTypeBV b v c tv r -> r0 # gmapQ :: (forall d. Data d => d -> u) -> RTypeBV b v c tv r -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTypeBV b v c tv r -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTypeBV b v c tv r -> m (RTypeBV b v c tv r) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTypeBV b v c tv r -> m (RTypeBV b v c tv r) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTypeBV b v c tv r -> m (RTypeBV b v c tv r) # | |||||||||
| Generic (RTypeBV b v c tv r) Source # | |||||||||
| (Hashable r, Hashable tv, Hashable c, Hashable v, Hashable b) => Hashable (RTypeBV b v c tv r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| 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 # | |||||||||
| (IsReft r, Subable r, TyConable c, Binder v, Variable r ~ v, ReftBind r ~ v) => Subable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp Associated Types
Methods syms :: RTPropBV v v c tv r -> [Variable (RTPropBV v v c tv r)] substa :: (Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r substf :: (Variable (RTPropBV v v c tv r) -> ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst :: SubstV (Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst1 :: RTPropBV v v c tv r -> (Variable (RTPropBV v v c tv r), ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r | |||||||||
| (Subable r, IsReft r, TyConable c, Binder v, Variable r ~ v, ReftBind r ~ v) => Subable (RTypeBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp Associated Types
Methods syms :: RTypeBV v v c tv r -> [Variable (RTypeBV v v c tv r)] substa :: (Variable (RTypeBV v v c tv r) -> Variable (RTypeBV v v c tv r)) -> RTypeBV v v c tv r -> RTypeBV v v c tv r substf :: (Variable (RTypeBV v v c tv r) -> ExprBV (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r))) -> RTypeBV v v c tv r -> RTypeBV v v c tv r subst :: SubstV (Variable (RTypeBV v v c tv r)) -> RTypeBV v v c tv r -> RTypeBV v v c tv r subst1 :: RTypeBV v v c tv r -> (Variable (RTypeBV v v c tv r), ExprBV (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r))) -> RTypeBV v v c tv r | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Meet (RTPropBV v v c tv r) Source # | |||||||||
| Top r => Top (RTypeBV b v c tv r) Source # | |||||||||
| type Variable (RRProp Reft) | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType type Variable (RRProp Reft) = Symbol | |||||||||
| type Rep (RTypeBV b v c tv r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type Variable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTPropBV v v c tv r) = v | |||||||||
| type Variable (RTypeBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTypeBV v v c tv r) = v | |||||||||
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 Symbol Symbol (RTProp BTyCon BTyVar r) Source # | |||||||||
| (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv NoReft)) => SubsTy tv ty (RTProp c tv (UReft r)) Source # | |||||||||
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- | ||||||||
Defined in Language.Haskell.Liquid.Types.RefType Associated Types
Methods syms :: RRProp Reft -> [Variable (RRProp Reft)] substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft | |||||||||
| (NFData τ, NFData t) => NFData (Ref τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Functor (RefB b τ) Source # | |||||||||
| Foldable (RefB b τ) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => RefB b τ m -> m # foldMap :: Monoid m => (a -> m) -> RefB b τ a -> m # foldMap' :: Monoid m => (a -> m) -> RefB b τ a -> m # foldr :: (a -> b0 -> b0) -> b0 -> RefB b τ a -> b0 # foldr' :: (a -> b0 -> b0) -> b0 -> RefB b τ a -> b0 # foldl :: (b0 -> a -> b0) -> b0 -> RefB b τ a -> b0 # foldl' :: (b0 -> a -> b0) -> b0 -> RefB b τ a -> b0 # foldr1 :: (a -> a -> a) -> RefB b τ a -> a # foldl1 :: (a -> a -> a) -> RefB b τ a -> a # elem :: Eq a => a -> RefB b τ a -> Bool # maximum :: Ord a => RefB b τ a -> a # minimum :: Ord a => RefB b τ a -> a # | |||||||||
| Traversable (RefB b τ) 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 | |||||||||
| REq t2 => REq (Ref t1 t2) Source # | |||||||||
| (Binary b, Binary τ, Binary t) => Binary (RefB b τ t) Source # | |||||||||
| (Eq b, Eq τ, Eq t) => Eq (RefB b τ t) Source # | |||||||||
| (Data b, Data τ, Data t) => Data (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> RefB b τ t -> c (RefB b τ t) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RefB b τ t) # toConstr :: RefB b τ t -> Constr # dataTypeOf :: RefB b τ t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (RefB b τ t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (RefB b τ t)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> RefB b τ t -> RefB b τ t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RefB b τ t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RefB b τ t -> r # gmapQ :: (forall d. Data d => d -> u) -> RefB b τ t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RefB b τ t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RefB b τ t -> m (RefB b τ t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RefB b τ t -> m (RefB b τ t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RefB b τ t -> m (RefB b τ t) # | |||||||||
| Generic (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # | |||||||||
| (Hashable b, Hashable τ, Hashable t) => Hashable (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Meet (RTProp BTyCon BTyVar NoReft) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar Reft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| ToReft t => ToReft (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Top t => Top (RefB b τ t) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTPropBV v v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTPropBV v v c tv r) Source # | |||||||||
| (IsReft r, Subable r, TyConable c, Binder v, Variable r ~ v, ReftBind r ~ v) => Subable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp Associated Types
Methods syms :: RTPropBV v v c tv r -> [Variable (RTPropBV v v c tv r)] substa :: (Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r substf :: (Variable (RTPropBV v v c tv r) -> ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst :: SubstV (Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst1 :: RTPropBV v v c tv r -> (Variable (RTPropBV v v c tv r), ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Meet (RTPropBV v v c tv r) Source # | |||||||||
| type Variable (RRProp Reft) | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType type Variable (RRProp Reft) = Symbol | |||||||||
| type Rep (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (RefB b τ t) = D1 ('MetaData "RefB" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "RProp" 'PrefixI 'True) (S1 ('MetaSel ('Just "rf_args") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(b, τ)]) :*: S1 ('MetaSel ('Just "rf_body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) | |||||||||
| type ReftBind (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type ReftVar (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type Variable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTPropBV v v c tv r) = v | |||||||||
type RTProp c tv r = RTPropV Symbol c tv r Source #
RTProp is a convenient alias for Ref that will save a bunch of typing.
In general, perhaps we need not expose Ref directly at all.
Instances
| NFData RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| NFData REnv Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.Types | |||||||||
| Monoid REnv Source # | |||||||||
| Semigroup REnv Source # | |||||||||
| Eq RTyVar Source # | Wrappers for GHC Type Elements -------------------------------------------- | ||||||||
| Ord RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| Data RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTyVar -> c RTyVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTyVar # toConstr :: RTyVar -> Constr # dataTypeOf :: RTyVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RTyVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTyVar) # gmapT :: (forall b. Data b => b -> b) -> RTyVar -> RTyVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTyVar -> r # gmapQ :: (forall d. Data d => d -> u) -> RTyVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTyVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTyVar -> m RTyVar # | |||||||||
| Exception Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String # backtraceDesired :: Error -> Bool # | |||||||||
| Generic RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Show RTyVar Source # | Printing Refinement Types ------------------------------------------------- | ||||||||
| Show Error Source # | |||||||||
| Hashable RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| Symbolic RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| PPrint RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| PPrint Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Expand SpecType Source # |
| ||||||||
| REq SpecType Source # | |||||||||
| Result Error Source # | |||||||||
| FreeVar RTyCon RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| SubsTy TyVar Type SpecType Source # | |||||||||
| SubsTy Symbol RSort Sort Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType | |||||||||
| 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 # | |||||||||
| (Freshable m Integer, Freshable m r, IsReft r, Subable r, Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => Freshable m (RRType r) Source # | |||||||||
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) RTyVar Source # | |||||||||
| SubsTy RTyVar (RType RTyCon RTyVar NoReft) (RTVar RTyVar (RType RTyCon RTyVar NoReft)) Source # | |||||||||
| Exception [Error] Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String # backtraceDesired :: [Error] -> Bool # | |||||||||
| PPrint (CtxError SpecType) Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- | ||||||||
Defined in Language.Haskell.Liquid.Types.RefType Associated Types
Methods syms :: RRProp Reft -> [Variable (RRProp Reft)] substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft | |||||||||
| Result [Error] Source # | |||||||||
| Meet (RTProp RTyCon RTyVar Reft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| Semigroup (RType RTyCon RTyVar r) => Meet (RType RTyCon RTyVar r) Source # | |||||||||
| type Rep RTyVar Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type Variable (RRProp Reft) | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType type Variable (RRProp Reft) = Symbol | |||||||||
type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, PPrint (ReftVar r), Fixpoint (ReftVar r), ToReft r, ReftBind r ~ Symbol, Eq c, Eq tv, Ord (ReftVar r), Hashable tv) Source #
type OkRTBV b v c tv r = (TyConable c, PPrint b, PPrint v, PPrint tv, PPrint c, PPrint r, PPrint (ReftVar r), Fixpoint b, Fixpoint v, Fixpoint (ReftVar r), Binder b, ToReft r, ReftBind r ~ b, Eq c, Eq tv, Ord b, Ord v, Ord (ReftVar r), Hashable tv) 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 # | |
Type Variables
Constructors
| RTVar | |
Fields
| |
Instances
| 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 # | |||||
| Functor (RTVar tv) Source # | |||||
| Foldable (RTVar tv) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => RTVar tv m -> m # foldMap :: Monoid m => (a -> m) -> RTVar tv a -> m # foldMap' :: Monoid m => (a -> m) -> RTVar tv a -> m # foldr :: (a -> b -> b) -> b -> RTVar tv a -> b # foldr' :: (a -> b -> b) -> b -> RTVar tv a -> b # foldl :: (b -> a -> b) -> b -> RTVar tv a -> b # foldl' :: (b -> a -> b) -> b -> RTVar tv a -> b # foldr1 :: (a -> a -> a) -> RTVar tv a -> a # foldl1 :: (a -> a -> a) -> RTVar tv a -> a # elem :: Eq a => a -> RTVar tv a -> Bool # maximum :: Ord a => RTVar tv a -> a # minimum :: Ord a => RTVar tv a -> a # | |||||
| Traversable (RTVar tv) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| (Binary s, Binary tv) => Binary (RTVar tv s) Source # | |||||
| (NFData tv, NFData s) => NFData (RTVar tv s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq tv => Eq (RTVar tv s) Source # | |||||
| (Data tv, Data s) => Data (RTVar tv s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType 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) # | |||||
| Generic (RTVar tv s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show tv => Show (RTVU c tv) Source # | |||||
| (Hashable tv, Hashable s) => Hashable (RTVar tv s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| PPrint v => PPrint (RTVar v s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| type Rep (RTVar tv s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (RTVar tv s) = D1 ('MetaData "RTVar" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.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 Source # | |||||
| Foldable RTVInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => RTVInfo m -> m # foldMap :: Monoid m => (a -> m) -> RTVInfo a -> m # foldMap' :: Monoid m => (a -> m) -> RTVInfo a -> m # foldr :: (a -> b -> b) -> b -> RTVInfo a -> b # foldr' :: (a -> b -> b) -> b -> RTVInfo a -> b # foldl :: (b -> a -> b) -> b -> RTVInfo a -> b # foldl' :: (b -> a -> b) -> b -> RTVInfo a -> b # foldr1 :: (a -> a -> a) -> RTVInfo a -> a # foldl1 :: (a -> a -> a) -> RTVInfo a -> a # elem :: Eq a => a -> RTVInfo a -> Bool # maximum :: Ord a => RTVInfo a -> a # minimum :: Ord a => RTVInfo a -> a # | |||||
| Traversable RTVInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Binary s => Binary (RTVInfo s) Source # | |||||
| NFData s => NFData (RTVInfo s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq s => Eq (RTVInfo s) Source # | |||||
| Data s => Data (RTVInfo s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTVInfo s -> c (RTVInfo s) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RTVInfo s) # toConstr :: RTVInfo s -> Constr # dataTypeOf :: RTVInfo s -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RTVInfo s)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RTVInfo s)) # gmapT :: (forall b. Data b => b -> b) -> RTVInfo s -> RTVInfo s # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTVInfo s -> r # gmapQ :: (forall d. Data d => d -> u) -> RTVInfo s -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RTVInfo s -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTVInfo s -> m (RTVInfo s) # | |||||
| Generic (RTVInfo s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Hashable s => Hashable (RTVInfo s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| type Rep (RTVInfo s) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (RTVInfo s) = D1 ('MetaData "RTVInfo" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "RTVNoInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "RTVInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rtv_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "rtv_kind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)) :*: (S1 ('MetaSel ('Just "rtv_is_val") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "rtv_is_pol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) | |||||
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s Source #
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 Source #
Predicate Variables
type PVar t = PVarV Symbol t Source #
Abstract Predicate Variables ----------------------------------
Instances
| SubsTy tv ty ty => SubsTy tv ty (PVarBV b v ty) Source # | |||||
| Functor (PVarBV b v) Source # | |||||
| (Binary v, Binary b, Binary t) => Binary (PVarBV b v t) Source # | |||||
| (NFData b, NFData v, NFData t) => NFData (PVarBV b v t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq b => Eq (PVarBV b v t) Source # | |||||
| Ord b => Ord (PVarBV b v t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| (Data t, Data v, Data b) => Data (PVarBV b v t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> PVarBV b v t -> c (PVarBV b v t) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PVarBV b v t) # toConstr :: PVarBV b v t -> Constr # dataTypeOf :: PVarBV b v t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (PVarBV b v t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (PVarBV b v t)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> PVarBV b v t -> PVarBV b v t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PVarBV b v t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PVarBV b v t -> r # gmapQ :: (forall d. Data d => d -> u) -> PVarBV b v t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PVarBV b v t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PVarBV b v t -> m (PVarBV b v t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PVarBV b v t -> m (PVarBV b v t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PVarBV b v t -> m (PVarBV b v t) # | |||||
| Generic (PVarBV b v t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| (Show t, Show v, Show b, Ord v, Ord b, Fixpoint v, Fixpoint b, Hashable b) => Show (PVarBV b v t) Source # | |||||
| Hashable b => Hashable (PVarBV b v a) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| (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 # | |||||
| type Rep (PVarBV b v t) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (PVarBV b v t) = D1 ('MetaData "PVarBV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "PV" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "ptype") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)) :*: (S1 ('MetaSel ('Just "parg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "pargs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(t, b, ExprBV b v)])))) | |||||
type Predicate = PredicateV Symbol Source #
type PredicateV v = PredicateBV Symbol v Source #
newtype PredicateBV b v Source #
Constructors
| Pr [UsedPVarBV b v] |
Instances
| NFData Predicate Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Monoid Predicate Source # | |||||||||
| Show Predicate Source # | |||||||||
| Meet Predicate Source # | |||||||||
| SubsTy tv RSort Predicate Source # | |||||||||
| (Binary v, Binary b) => Binary (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods put :: PredicateBV b v -> Put # get :: Get (PredicateBV b v) # putList :: [PredicateBV b v] -> Put # | |||||||||
| Eq b => Semigroup (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods (<>) :: PredicateBV b v -> PredicateBV b v -> PredicateBV b v # sconcat :: NonEmpty (PredicateBV b v) -> PredicateBV b v # stimes :: Integral b0 => b0 -> PredicateBV b v -> PredicateBV b v # | |||||||||
| (Ord b, Ord v) => Eq (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods (==) :: PredicateBV b v -> PredicateBV b v -> Bool # (/=) :: PredicateBV b v -> PredicateBV b v -> Bool # | |||||||||
| (Data v, Data b) => Data (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> PredicateBV b v -> c (PredicateBV b v) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PredicateBV b v) # toConstr :: PredicateBV b v -> Constr # dataTypeOf :: PredicateBV b v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PredicateBV b v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PredicateBV b v)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> PredicateBV b v -> PredicateBV b v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateBV b v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateBV b v -> r # gmapQ :: (forall d. Data d => d -> u) -> PredicateBV b v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PredicateBV b v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredicateBV b v -> m (PredicateBV b v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredicateBV b v -> m (PredicateBV b v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredicateBV b v -> m (PredicateBV b v) # | |||||||||
| Generic (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods from :: PredicateBV b v -> Rep (PredicateBV b v) x # to :: Rep (PredicateBV b v) x -> PredicateBV b v # | |||||||||
| (Ord b, Ord v, Hashable b) => Hashable (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| (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 # | |||||||||
| Hashable v => Subable (PredicateBV v v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods syms :: PredicateBV v v -> [Variable (PredicateBV v v)] substa :: (Variable (PredicateBV v v) -> Variable (PredicateBV v v)) -> PredicateBV v v -> PredicateBV v v substf :: (Variable (PredicateBV v v) -> ExprBV (Variable (PredicateBV v v)) (Variable (PredicateBV v v))) -> PredicateBV v v -> PredicateBV v v subst :: SubstV (Variable (PredicateBV v v)) -> PredicateBV v v -> PredicateBV v v subst1 :: PredicateBV v v -> (Variable (PredicateBV v v), ExprBV (Variable (PredicateBV v v)) (Variable (PredicateBV v v))) -> PredicateBV v v | |||||||||
| (Binder b, Ord v, PredicateCompat b v) => ToReft (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods toReft :: PredicateBV b v -> ReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v)) Source # toUReft :: PredicateBV b v -> UReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v)) (ReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v))) Source # | |||||||||
| Top (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods top :: PredicateBV b v -> PredicateBV b v Source # | |||||||||
| type Rep (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type Variable (PredicateBV v v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Variable (PredicateBV v v) = v | |||||||||
| type ReftBind (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type ReftVar (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
class PredicateCompat b v where Source #
Instances
| PredicateCompat Symbol LocSymbol Source # | |
| PredicateCompat Symbol Symbol Source # | |
Expression Arguments
notExprArg :: RTypeV v c tv r -> Bool Source #
Manipulating Predicates
emapExprVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v') Source #
A map traversal that collects the local variables in scope
mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v' Source #
emapPredicateVM :: Monad m => ([Symbol] -> v -> m v') -> PredicateV v -> m (PredicateV v') Source #
A map traversal that collects the local variables in scope
emapPVarVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t') Source #
A map traversal that collects the local variables in scope
emapSubstVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> KVarSubst b v -> m (KVarSubst b v') Source #
pvars :: PredicateBV b v -> [UsedPVarBV b v] Source #
pApp :: PredicateCompat b v => v -> [ExprBV b v] -> ExprBV b v Source #
Refinements
Constructors
| MkUReft | |
Fields
| |
Instances
| NFData REnv Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.Types | |||||||||
| Monoid REnv Source # | |||||||||
| Semigroup REnv Source # | |||||||||
| Ord DataDecl Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.DataDecl | |||||||||
| Exception Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String # backtraceDesired :: Error -> Bool # | |||||||||
| Show BareSpec Source # | |||||||||
| Show Error Source # | |||||||||
| PPrint Error Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Expand DataCtor Source # | |||||||||
| Expand DataDecl Source # | |||||||||
| Expand BareType Source # |
| ||||||||
| Expand RReft Source # | |||||||||
| Expand SpecType Source # |
| ||||||||
| Expand BareDef Source # | |||||||||
| Expand BareMeasure Source # | |||||||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source # | |||||||||
| Expand BareSpec Source # | |||||||||
| Expand BareRTAlias Source # | |||||||||
Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source # | |||||||||
| REq SpecType Source # | |||||||||
| Result Error Source # | |||||||||
| Freshable m Integer => Freshable m RReft Source # | |||||||||
| SubsTy TyVar Type SpecType Source # | |||||||||
| SubsTy RTyVar RSort SpecType Source # | |||||||||
| SubsTy RTyVar RTyVar SpecType Source # | |||||||||
| SubsTy tv ty r => SubsTy tv ty (UReft r) Source # | |||||||||
| (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv NoReft)) => SubsTy tv ty (RTProp c tv (UReft r)) Source # | |||||||||
| NFData r => NFData (UReft r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Monoid a => Monoid (UReft a) Source # | |||||||||
| Exception [Error] Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy Methods toException :: [Error] -> SomeException # fromException :: SomeException -> Maybe [Error] # displayException :: [Error] -> String # backtraceDesired :: [Error] -> Bool # | |||||||||
| PPrint (UReft r) => Show (UReft r) Source # | |||||||||
| PPrint (CtxError SpecType) Source # | |||||||||
Defined in Language.Haskell.Liquid.UX.Tidy | |||||||||
| Expression (UReft ()) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| REq (UReft Reft) Source # | |||||||||
| Result [Error] Source # | |||||||||
| Functor (UReftBV b v) Source # | |||||||||
| Foldable (UReftBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => UReftBV b v m -> m # foldMap :: Monoid m => (a -> m) -> UReftBV b v a -> m # foldMap' :: Monoid m => (a -> m) -> UReftBV b v a -> m # foldr :: (a -> b0 -> b0) -> b0 -> UReftBV b v a -> b0 # foldr' :: (a -> b0 -> b0) -> b0 -> UReftBV b v a -> b0 # foldl :: (b0 -> a -> b0) -> b0 -> UReftBV b v a -> b0 # foldl' :: (b0 -> a -> b0) -> b0 -> UReftBV b v a -> b0 # foldr1 :: (a -> a -> a) -> UReftBV b v a -> a # foldl1 :: (a -> a -> a) -> UReftBV b v a -> a # toList :: UReftBV b v a -> [a] # null :: UReftBV b v a -> Bool # length :: UReftBV b v a -> Int # elem :: Eq a => a -> UReftBV b v a -> Bool # maximum :: Ord a => UReftBV b v a -> a # minimum :: Ord a => UReftBV b v a -> a # | |||||||||
| Traversable (UReftBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| (Binary v, Binary b, Binary r) => Binary (UReftBV b v r) Source # | |||||||||
| (Semigroup a, Eq b) => Semigroup (UReftBV b v a) Source # | |||||||||
| (Ord b, Ord v, Eq r) => Eq (UReftBV b v r) Source # | |||||||||
| (Data r, Data v, Data b) => Data (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> UReftBV b v r -> c (UReftBV b v r) # gunfold :: (forall b0 r0. Data b0 => c (b0 -> r0) -> c r0) -> (forall r1. r1 -> c r1) -> Constr -> c (UReftBV b v r) # toConstr :: UReftBV b v r -> Constr # dataTypeOf :: UReftBV b v r -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (UReftBV b v r)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UReftBV b v r)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> UReftBV b v r -> UReftBV b v r # gmapQl :: (r0 -> r' -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReftBV b v r -> r0 # gmapQr :: forall r0 r'. (r' -> r0 -> r0) -> r0 -> (forall d. Data d => d -> r') -> UReftBV b v r -> r0 # gmapQ :: (forall d. Data d => d -> u) -> UReftBV b v r -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UReftBV b v r -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UReftBV b v r -> m (UReftBV b v r) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UReftBV b v r -> m (UReftBV b v r) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UReftBV b v r -> m (UReftBV b v r) # | |||||||||
| Generic (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| (Ord b, Ord v, Hashable r, Hashable b) => Hashable (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| (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 # | |||||||||
| (Subable r, Variable r ~ v) => Subable (UReftBV v v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods syms :: UReftBV v v r -> [Variable (UReftBV v v r)] substa :: (Variable (UReftBV v v r) -> Variable (UReftBV v v r)) -> UReftBV v v r -> UReftBV v v r substf :: (Variable (UReftBV v v r) -> ExprBV (Variable (UReftBV v v r)) (Variable (UReftBV v v r))) -> UReftBV v v r -> UReftBV v v r subst :: SubstV (Variable (UReftBV v v r)) -> UReftBV v v r -> UReftBV v v r subst1 :: UReftBV v v r -> (Variable (UReftBV v v r), ExprBV (Variable (UReftBV v v r)) (Variable (UReftBV v v r))) -> UReftBV v v r | |||||||||
| (IsReft r, Binder v, ReftBind r ~ v, ReftVar r ~ v) => IsReft (UReftBV v v r) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| Meet (RType BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| (Meet r, Eq v) => Meet (UReftBV v v r) Source # | |||||||||
| (ToReft r, ReftBind r ~ b, ReftVar r ~ v) => ToReft (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Top r => Top (UReftBV b v r) Source # | |||||||||
| type Rep (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (UReftBV b v r) = D1 ('MetaData "UReftBV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "MkUReft" 'PrefixI 'True) (S1 ('MetaSel ('Just "ur_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 r) :*: S1 ('MetaSel ('Just "ur_pred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (PredicateBV b v)))) | |||||||||
| type Variable (UReftBV v v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Variable (UReftBV v v r) = v | |||||||||
| type ReftBind (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type ReftVar (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
emapUReftVM :: Monad m => ([Symbol] -> v -> m v') -> (r -> m r') -> UReftV v r -> m (UReftV v' r') Source #
Constructors
| NoReft |
Instances
| Functor NoReftB Source # | |||||||||
| Foldable NoReftB Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => NoReftB m -> m # foldMap :: Monoid m => (a -> m) -> NoReftB a -> m # foldMap' :: Monoid m => (a -> m) -> NoReftB a -> m # foldr :: (a -> b -> b) -> b -> NoReftB a -> b # foldr' :: (a -> b -> b) -> b -> NoReftB a -> b # foldl :: (b -> a -> b) -> b -> NoReftB a -> b # foldl' :: (b -> a -> b) -> b -> NoReftB a -> b # foldr1 :: (a -> a -> a) -> NoReftB a -> a # foldl1 :: (a -> a -> a) -> NoReftB a -> a # elem :: Eq a => a -> NoReftB a -> Bool # maximum :: Ord a => NoReftB a -> a # minimum :: Ord a => NoReftB a -> a # | |||||||||
| Traversable NoReftB Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| 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 tv RSort Predicate Source # | |||||||||
| SubsTy tv ty NoReft Source # | |||||||||
| SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) 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 # | |||||||||
| Binary (NoReftB b) Source # | |||||||||
| NFData (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Monoid (NoReftB b) Source # | |||||||||
| Semigroup (NoReftB b) Source # | |||||||||
| Eq (NoReftB b) Source # | |||||||||
| Data b => Data (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> NoReftB b -> c (NoReftB b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NoReftB b) # toConstr :: NoReftB b -> Constr # dataTypeOf :: NoReftB b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NoReftB b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NoReftB b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> NoReftB b -> NoReftB b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NoReftB b -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NoReftB b -> r # gmapQ :: (forall d. Data d => d -> u) -> NoReftB b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NoReftB b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NoReftB b -> m (NoReftB b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NoReftB b -> m (NoReftB b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NoReftB b -> m (NoReftB b) # | |||||||||
| Generic (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Hashable (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| PPrint (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| Hashable b => Subable (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods syms :: NoReftB b -> [Variable (NoReftB b)] substa :: (Variable (NoReftB b) -> Variable (NoReftB b)) -> NoReftB b -> NoReftB b substf :: (Variable (NoReftB b) -> ExprBV (Variable (NoReftB b)) (Variable (NoReftB b))) -> NoReftB b -> NoReftB b subst :: SubstV (Variable (NoReftB b)) -> NoReftB b -> NoReftB b subst1 :: NoReftB b -> (Variable (NoReftB b), ExprBV (Variable (NoReftB b)) (Variable (NoReftB b))) -> NoReftB b | |||||||||
| Subable (RRProp Reft) | Subable Instances ----------------------------------------------------- | ||||||||
Defined in Language.Haskell.Liquid.Types.RefType Associated Types
Methods syms :: RRProp Reft -> [Variable (RRProp Reft)] substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft | |||||||||
| Expand (BRType NoReft) Source # | |||||||||
| Expand (NoReftB b) Source # | |||||||||
| Binder b => IsReft (NoReftB b) Source # | |||||||||
| Meet (NoReftB b) Source # | |||||||||
| Binder b => ToReft (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Top (NoReftB b) Source # | |||||||||
| Show tv => Show (RTVU c tv) Source # | |||||||||
| (Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c) => Eq (RType c tv NoReft) Source # | |||||||||
| PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar NoReft) Source # | |||||||||
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar Reft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |||||||||
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTPropBV v v c tv r) Source # | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTPropBV v v c tv r) Source # | |||||||||
| (IsReft r, Subable r, TyConable c, Binder v, Variable r ~ v, ReftBind r ~ v) => Subable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp Associated Types
Methods syms :: RTPropBV v v c tv r -> [Variable (RTPropBV v v c tv r)] substa :: (Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r substf :: (Variable (RTPropBV v v c tv r) -> ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst :: SubstV (Variable (RTPropBV v v c tv r)) -> RTPropBV v v c tv r -> RTPropBV v v c tv r subst1 :: RTPropBV v v c tv r -> (Variable (RTPropBV v v c tv r), ExprBV (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))) -> RTPropBV v v c tv r | |||||||||
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Meet (RTPropBV v v c tv r) Source # | |||||||||
| type Rep (NoReftB b) Source # | |||||||||
| type Variable (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType type Variable (NoReftB b) = b | |||||||||
| type Variable (RRProp Reft) | |||||||||
Defined in Language.Haskell.Liquid.Types.RefType type Variable (RRProp Reft) = Symbol | |||||||||
| type ReftBind (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type ReftVar (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType | |||||||||
| type Variable (RTPropBV v v c tv r) | |||||||||
Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTPropBV v v c tv r) = v | |||||||||
Parse-time entities describing refined data types
Constructors
| IdSizeFun | x -> F.EVar x |
| SymSizeFun (Located v) | x -> f x |
Instances
| Functor SizeFunV Source # | |||||
| Foldable SizeFunV Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods fold :: Monoid m => SizeFunV m -> m # foldMap :: Monoid m => (a -> m) -> SizeFunV a -> m # foldMap' :: Monoid m => (a -> m) -> SizeFunV a -> m # foldr :: (a -> b -> b) -> b -> SizeFunV a -> b # foldr' :: (a -> b -> b) -> b -> SizeFunV a -> b # foldl :: (b -> a -> b) -> b -> SizeFunV a -> b # foldl' :: (b -> a -> b) -> b -> SizeFunV a -> b # foldr1 :: (a -> a -> a) -> SizeFunV a -> a # foldl1 :: (a -> a -> a) -> SizeFunV a -> a # elem :: Eq a => a -> SizeFunV a -> Bool # maximum :: Ord a => SizeFunV a -> a # minimum :: Ord a => SizeFunV a -> a # | |||||
| Traversable SizeFunV Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Binary v => Binary (SizeFunV v) Source # | |||||
| NFData v => NFData (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq v => Eq (SizeFunV v) Source # | |||||
| Data v => Data (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SizeFunV v -> c (SizeFunV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SizeFunV v) # toConstr :: SizeFunV v -> Constr # dataTypeOf :: SizeFunV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SizeFunV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SizeFunV v)) # gmapT :: (forall b. Data b => b -> b) -> SizeFunV v -> SizeFunV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SizeFunV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SizeFunV v -> r # gmapQ :: (forall d. Data d => d -> u) -> SizeFunV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SizeFunV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SizeFunV v -> m (SizeFunV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFunV v -> m (SizeFunV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SizeFunV v -> m (SizeFunV v) # | |||||
| Generic (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show v => Show (SizeFunV v) Source # | |||||
| Hashable v => Hashable (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| PPrint v => PPrint (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| type Rep (SizeFunV v) Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep (SizeFunV v) = D1 ('MetaData "SizeFunV" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.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 (Located v)))) | |||||
Constructors
| TyConP | |
Fields
| |
Instances
| Data TyConP Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyConP -> c TyConP # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyConP # toConstr :: TyConP -> Constr # dataTypeOf :: TyConP -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyConP) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyConP) # gmapT :: (forall b. Data b => b -> b) -> TyConP -> TyConP # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyConP -> r # gmapQ :: (forall d. Data d => d -> u) -> TyConP -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyConP -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyConP -> m TyConP # | |||||
| Generic TyConP Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show TyConP Source # | |||||
| PPrint TyConP Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Loc TyConP Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| type Rep TyConP Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType type Rep TyConP = D1 ('MetaData "TyConP" "Language.Haskell.Liquid.Types.RType" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "TyConP" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tcpLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "tcpCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Just "tcpFreeTyVarsTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RTyVar]))) :*: ((S1 ('MetaSel ('Just "tcpFreePredTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [PVar RSort]) :*: S1 ('MetaSel ('Just "tcpVarianceTs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo)) :*: (S1 ('MetaSel ('Just "tcpVariancePs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 VarianceInfo) :*: S1 ('MetaSel ('Just "tcpSizeFun") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SizeFun)))))) | |||||
Pre-instantiated RType
type RTVU c tv = RTVUV Symbol c tv Source #
Unified Representation of Refinement Types --------------------------------
Instantiated RType
type BareTypeLHName = BareTypeV LHName Source #
type BareTypeParsed = BareTypeV LocSymbol Source #
type LocBareType = Located BareType Source #
type LocSpecType = Located SpecType Source #
type UsedPVar = UsedPVarV Symbol Source #
Predicates ----------------------------------------------------------------
Printer Configuration
Printer ----------------------------------------------------------------
Constructors
| PP | |
ppEnvShort :: PPEnv -> PPEnv Source #
Refined Function Info
Instances
| Binary RFInfo Source # | |||||
| NFData RFInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| Eq RFInfo Source # | |||||
| Data RFInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RFInfo -> c RFInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RFInfo # toConstr :: RFInfo -> Constr # dataTypeOf :: RFInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RFInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RFInfo) # gmapT :: (forall b. Data b => b -> b) -> RFInfo -> RFInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RFInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> RFInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RFInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RFInfo -> m RFInfo # | |||||
| Generic RFInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||
| Show RFInfo Source # | |||||
| Hashable RFInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
| type Rep RFInfo Source # | |||||
Defined in Language.Haskell.Liquid.Types.RType | |||||
classRFInfo :: Bool -> RFInfo Source #
Converting to and from refinements
class (Binder (ReftBind r), Eq (ReftVar r)) => ToReft r where Source #
Types that have one associated refinement representible by a ReftBV
Minimal complete definition
Methods
toReft :: r -> ReftBV (ReftBind r) (ReftVar r) Source #
toUReft :: r -> UReftBV (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r)) Source #
Instances
| ToReft () Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| Binder b => ToReft (NoReftB b) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| (Binder b, Eq v) => ToReft (ReftBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| (Binder b, Ord v, PredicateCompat b v) => ToReft (PredicateBV b v) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
Methods toReft :: PredicateBV b v -> ReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v)) Source # toUReft :: PredicateBV b v -> UReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v)) (ReftBV (ReftBind (PredicateBV b v)) (ReftVar (PredicateBV b v))) Source # | |||||||||
| ToReft t => ToReft (RefB b τ t) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
| (ToReft r, ReftBind r ~ b, ReftVar r ~ v) => ToReft (UReftBV b v r) Source # | |||||||||
Defined in Language.Haskell.Liquid.Types.RType Associated Types
| |||||||||
class Semigroup r => Meet r where Source #
Types that can be combined conjunctively in some sense
Minimal complete definition
Nothing
Instances
| Meet Predicate Source # | |
| Meet () Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| Meet (NoReftB b) Source # | |
| (Binder v, Fixpoint v) => Meet (ReftBV v v) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| Meet (RTProp BTyCon BTyVar NoReft) Source # | |
| Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # | |
| Meet (RTProp RTyCon RTyVar Reft) Source # | |
| Meet (RTProp RTyCon RTyVar NoReft) Source # | |
| Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # | |
| Meet (RType BTyCon BTyVar (UReft Reft)) Source # | |
| Semigroup (RType RTyCon RTyVar r) => Meet (RType RTyCon RTyVar r) Source # | |
| (Meet r, Eq v) => Meet (UReftBV v v r) Source # | |
| (SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Meet (RTPropBV v v c tv r) Source # | |
Types whose refinements can be cleared to true
Instances
| Top () Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| Top (NoReftB b) Source # | |
| Binder b => Top (ReftBV b v) Source # | |
Defined in Language.Haskell.Liquid.Types.RType | |
| Top (PredicateBV b v) Source # | |
Defined in Language.Haskell.Liquid.Types.RType Methods top :: PredicateBV b v -> PredicateBV b v Source # | |
| Top t => Top (RefB b τ t) Source # | |
| Top r => Top (UReftBV b v r) Source # | |
| Top r => Top (RTypeBV b v c tv r) Source # | |
class (ToReft r, Meet r, Top r) => IsReft r where Source #
Types that can be constructed from a ReftBV