Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.RTypeOp

Contents

Constructing & Destructing RTypes
Traversing RType
Converting To and From Sort
Some tests on RTypes
Scoping Info
Misc
Orphan instances

Description

This module should contain all the global type definitions and basic instances.

Synopsis

type SpecRep = RRep RReft
type RTypeRep = RTypeRepV Symbol
type RTypeRepV = RTypeRepBV Symbol
data RTypeRepBV b v c tv r = RTypeRep {
- ty_vars :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
- ty_preds :: [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
- ty_binds :: [b]
- ty_info :: [RFInfo]
- ty_refts :: [r]
- ty_args :: [RTypeBV b v c tv r]
- ty_res :: RTypeBV b v c tv r
}
fromRTypeRep :: RTypeRepBV b v c tv r -> RTypeBV b v c tv r
toRTypeRep :: RTypeBV b v c tv r -> RTypeRepBV b v c tv r
mkArrow :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)] -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))] -> [(b, RFInfo, RTypeBV b v c tv r, r)] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrow :: RTypeBV b v t t1 a -> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
mkUnivs :: (Foldable t, Foldable t1) => t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r) -> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b))) -> RTypeBV b v c tv r -> RTypeBV b v c tv r
bkUniv :: RTypeBV b v tv c r -> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)], [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkClass :: (PPrint c, TyConable c) => RTypeBV b v c tv r -> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])], SpecType)
bkUnivClass' :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType)
rFun :: IsReft r => b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun' :: IsReft r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rCls :: IsReft r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rRCls :: IsReft r => c -> [RType c tv r] -> RType c tv r
rFunDebug :: IsReft r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
classRFInfoType :: Bool -> RType c tv r -> RType c tv r
efoldReft :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (c -> [RTypeBV b v c tv r] -> [(b, a)]) -> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)]) -> (RTypeBV b v c tv r -> a) -> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z) -> (PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> SEnvB b a -> SEnvB b a) -> SEnvB b a -> z -> RTypeBV b v c tv r -> z
foldReft :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z) -> z -> RTypeBV b v c tv r -> z
foldReft' :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (RTypeBV b v c tv r -> a) -> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z) -> z -> RTypeBV b v c tv r -> z
emapReft :: ([b] -> r1 -> r2) -> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft :: (r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r)
emapReftM :: (Monad m, ToReft r1, Binder b, CompatibleBinder b tv, ReftBind r1 ~ b) => Bool -> ([b] -> v1 -> m v2) -> ([b] -> r1 -> m r2) -> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
emapRefM :: (Monad m, ToReft t, Binder b, CompatibleBinder b tv, ReftBind t ~ b) => Bool -> ([b] -> v -> m v') -> ([b] -> t -> m s) -> [b] -> RTPropBV b v c tv t -> m (RTPropBV b v' c tv s)
mapExprReft :: (b -> ExprBV b v -> ExprBV b v) -> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBind :: (Hashable b, Hashable b') => (b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
emapFReftM :: Monad m => ([Symbol] -> v -> m v') -> ReftV v -> m (ReftV v')
mapRTypeV :: (v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeVM :: (Hashable b, Monad m) => (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapDataDeclV :: (v -> v') -> DataDeclP v ty -> DataDeclP v' ty
mapDataDeclVM :: Monad m => (v -> m v') -> DataDeclP v ty -> m (DataDeclP v' ty)
emapDataDeclM :: Monad m => Bool -> ([Symbol] -> v -> m v') -> ([Symbol] -> ty -> m ty') -> DataDeclP v ty -> m (DataDeclP v' ty')
emapDataCtorTyM :: Monad m => ([Symbol] -> ty -> m ty') -> DataCtorP ty -> m (DataCtorP ty')
emapBareTypeVM :: (Monad m, Ord v1) => Bool -> ([Symbol] -> v1 -> m v2) -> [Symbol] -> BareTypeV v1 -> m (BareTypeV v2)
parsedToBareType :: BareTypeParsed -> BareType
ofRSort :: IsReft r => RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
toRSort :: Binder b => RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
rTypeValueVar :: (ToReft r, Binder (ReftBind r)) => RTypeBV b v c tv r -> ReftBind r
rTypeReft :: (ToReft r, Binder (ReftBind r)) => RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
stripRTypeBase :: RTypeBV b v c tv r -> Maybe r
topRTypeBase :: Top r => RType c tv r -> RType c tv r
isBase :: RType t t1 t2 -> Bool
isFunTy :: RType t t1 t2 -> Bool
isTrivial :: (ToReft r, TyConable c, Binder b, ReftBind r ~ b) => RTypeBV b v c tv r -> Bool
hasHoleTy :: RType t t1 t2 -> Bool
type BScope = Bool
addInvCond :: SpecType -> RReft -> SpecType
insertsSEnv :: (Eq b, Hashable b) => SEnvB b a -> [(b, a)] -> SEnvB b a

Constructing & Destructing RTypes

type SpecRep = RRep RReft Source #

type RTypeRep = RTypeRepV Symbol Source #

type RTypeRepV = RTypeRepBV Symbol Source #

data RTypeRepBV b v c tv r Source #

Constructors

RTypeRep
Fields ty_vars :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)] ty_preds :: [PVarBV b v (RTypeBV b v c tv (NoReftB b))] ty_binds :: [b] ty_info :: [RFInfo] ty_refts :: [r] ty_args :: [RTypeBV b v c tv r] ty_res :: RTypeBV b v c tv r

fromRTypeRep :: RTypeRepBV b v c tv r -> RTypeBV b v c tv r Source #

toRTypeRep :: RTypeBV b v c tv r -> RTypeRepBV b v c tv r Source #

mkArrow :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)] -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))] -> [(b, RFInfo, RTypeBV b v c tv r, r)] -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

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

bkArrow :: RTypeBV b v t t1 a -> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a) Source #

safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a) Source #

mkUnivs :: (Foldable t, Foldable t1) => t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r) -> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b))) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

bkUniv :: RTypeBV b v tv c r -> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)], [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r) Source #

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

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

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

rFun :: IsReft r => b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

rFun' :: IsReft r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

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

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

rFunDebug :: IsReft r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source #

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

Traversing `RType`

efoldReft :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (c -> [RTypeBV b v c tv r] -> [(b, a)]) -> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)]) -> (RTypeBV b v c tv r -> a) -> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z) -> (PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> SEnvB b a -> SEnvB b a) -> SEnvB b a -> z -> RTypeBV b v c tv r -> z Source #

foldReft :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z) -> z -> RTypeBV b v c tv r -> z Source #

foldReft' :: (IsReft r, TyConable c, Binder b, ReftBind r ~ b) => BScope -> (RTypeBV b v c tv r -> a) -> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z) -> z -> RTypeBV b v c tv r -> z Source #

emapReft :: ([b] -> r1 -> r2) -> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2 Source #

mapReft :: (r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2 Source #

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

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

emapReftM :: (Monad m, ToReft r1, Binder b, CompatibleBinder b tv, ReftBind r1 ~ b) => Bool -> ([b] -> v1 -> m v2) -> ([b] -> r1 -> m r2) -> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2) Source #

emapRefM :: (Monad m, ToReft t, Binder b, CompatibleBinder b tv, ReftBind t ~ b) => Bool -> ([b] -> v -> m v') -> ([b] -> t -> m s) -> [b] -> RTPropBV b v c tv t -> m (RTPropBV b v' c tv s) Source #

mapExprReft :: (b -> ExprBV b v -> ExprBV b v) -> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v) Source #

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

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

mapBind :: (Hashable b, Hashable b') => (b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r Source #

mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r Source #

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

emapFReftM :: Monad m => ([Symbol] -> v -> m v') -> ReftV v -> m (ReftV v') Source #

mapRTypeV :: (v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r Source #

mapRTypeVM :: (Hashable b, Monad m) => (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r) Source #

mapDataDeclV :: (v -> v') -> DataDeclP v ty -> DataDeclP v' ty Source #

mapDataDeclVM :: Monad m => (v -> m v') -> DataDeclP v ty -> m (DataDeclP v' ty) Source #

emapDataDeclM :: Monad m => Bool -> ([Symbol] -> v -> m v') -> ([Symbol] -> ty -> m ty') -> DataDeclP v ty -> m (DataDeclP v' ty') Source #

emapDataCtorTyM :: Monad m => ([Symbol] -> ty -> m ty') -> DataCtorP ty -> m (DataCtorP ty') Source #

emapBareTypeVM :: (Monad m, Ord v1) => Bool -> ([Symbol] -> v1 -> m v2) -> [Symbol] -> BareTypeV v1 -> m (BareTypeV v2) Source #

parsedToBareType :: BareTypeParsed -> BareType Source #

Converting To and From Sort

ofRSort :: IsReft r => RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r Source #

toRSort :: Binder b => RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b) Source #

rTypeValueVar :: (ToReft r, Binder (ReftBind r)) => RTypeBV b v c tv r -> ReftBind r Source #

rTypeReft :: (ToReft r, Binder (ReftBind r)) => RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r) Source #

stripRTypeBase :: RTypeBV b v c tv r -> Maybe r Source #

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

Some tests on RTypes

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

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

isTrivial :: (ToReft r, TyConable c, Binder b, ReftBind r ~ b) => RTypeBV b v c tv r -> Bool Source #

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

Scoping Info

type BScope = Bool Source #

Information about scope Binders Scope in

Misc

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

insertsSEnv :: (Eq b, Hashable b) => SEnvB b a -> [(b, a)] -> SEnvB b a Source #

Orphan instances

(IsReft r, Subable r, TyConable c, Binder v, Variable r ~ v, ReftBind r ~ v) => Subable (RTPropBV v v c tv r) Source #

Instance details

Associated Types

type Variable (RTPropBV v v c tv r)
Instance details Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTPropBV v v c tv r) = v

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

Instance details

Associated Types

type Variable (RTypeBV v v c tv r)
Instance details Defined in Language.Haskell.Liquid.Types.RTypeOp type Variable (RTypeBV v v c tv r) = v

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

Top r => Top (RTypeBV b v c tv r) Source #

Instance details

Methods

top :: RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

Constructing & Destructing RTypes

Traversing RType

Converting To and From Sort

Some tests on RTypes

Scoping Info

Misc

Orphan instances

Traversing `RType`