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
data RTypeRepV v c tv r = RTypeRep {
- ty_vars :: [(RTVar tv (RTypeV v c tv ()), r)]
- ty_preds :: [PVarV v (RTypeV v c tv ())]
- ty_binds :: [Symbol]
- ty_info :: [RFInfo]
- ty_refts :: [r]
- ty_args :: [RTypeV v c tv r]
- ty_res :: RTypeV v c tv r
}
fromRTypeRep :: RTypeRepV v c tv r -> RTypeV v c tv r
toRTypeRep :: RTypeV v c tv r -> RTypeRepV v c tv r
mkArrow :: [(RTVar tv (RTypeV v c tv ()), r)] -> [PVarV v (RTypeV v c tv ())] -> [(Symbol, RFInfo, RTypeV v c tv r, r)] -> RTypeV v c tv r -> RTypeV v c tv r
bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrow :: RTypeV v t t1 a -> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV 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 (RTypeV v c tv ()), r) -> t1 (PVarV v (RTypeV v c tv ())) -> RTypeV v c tv r -> RTypeV v c tv r
bkUniv :: RTypeV v tv c r -> ([(RTVar c (RTypeV v tv c ()), r)], [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkClass :: (PPrint c, TyConable c) => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])], SpecType)
bkUnivClass' :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType)
rFun :: Monoid r => Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun' :: Monoid r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r
rFunDebug :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
classRFInfoType :: Bool -> RType c tv r -> RType c tv r
efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b
foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft :: (r1 -> r2) -> RTypeV v c tv r1 -> RTypeV 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, ToReftV r1, Symbolic tv) => Bool -> ([Symbol] -> v1 -> m v2) -> ([Symbol] -> r1 -> m r2) -> [Symbol] -> RTypeV v1 c tv r1 -> m (RTypeV v2 c tv r2)
emapRefM :: (Monad m, ToReftV t, Symbolic tv) => Bool -> ([Symbol] -> v -> m v') -> ([Symbol] -> t -> m s) -> [Symbol] -> RTPropV v c tv t -> m (RTPropV v' c tv s)
mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBind :: (Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV 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') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeVM :: Monad m => (v -> m v') -> RTypeV v c tv r -> m (RTypeV 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 => Bool -> ([Symbol] -> v1 -> m v2) -> [Symbol] -> BareTypeV v1 -> m (BareTypeV v2)
parsedToBareType :: BareTypeParsed -> BareType
ofRSort :: Reftable r => RType c tv () -> RType c tv r
toRSort :: RTypeV v c tv r -> RTypeV v c tv ()
rTypeValueVar :: Reftable r => RType c tv r -> Symbol
rTypeReft :: Reftable r => RType c tv r -> Reft
stripRTypeBase :: RType c tv r -> Maybe r
topRTypeBase :: Reftable r => RType c tv r -> RType c tv r
isBase :: RType t t1 t2 -> Bool
isFunTy :: RType t t1 t2 -> Bool
isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool
hasHoleTy :: RType t t1 t2 -> Bool
type BScope = Bool
addInvCond :: SpecType -> RReft -> SpecType
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a

Constructing & Destructing RTypes

type SpecRep = RRep RReft Source #

type RTypeRep = RTypeRepV Symbol Source #

data RTypeRepV v c tv r Source #

Constructors

RTypeRep
Fields ty_vars :: [(RTVar tv (RTypeV v c tv ()), r)] ty_preds :: [PVarV v (RTypeV v c tv ())] ty_binds :: [Symbol] ty_info :: [RFInfo] ty_refts :: [r] ty_args :: [RTypeV v c tv r] ty_res :: RTypeV v c tv r

fromRTypeRep :: RTypeRepV v c tv r -> RTypeV v c tv r Source #

toRTypeRep :: RTypeV v c tv r -> RTypeRepV v c tv r Source #

mkArrow :: [(RTVar tv (RTypeV v c tv ()), r)] -> [PVarV v (RTypeV v c tv ())] -> [(Symbol, RFInfo, RTypeV v c tv r, r)] -> RTypeV v c tv r -> RTypeV v c tv r Source #

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

bkArrow :: RTypeV v t t1 a -> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV 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 (RTypeV v c tv ()), r) -> t1 (PVarV v (RTypeV v c tv ())) -> RTypeV v c tv r -> RTypeV v c tv r Source #

bkUniv :: RTypeV v tv c r -> ([(RTVar c (RTypeV v tv c ()), r)], [PVarV v (RTypeV v tv c ())], RTypeV v tv c r) Source #

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

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

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

rFun :: Monoid r => Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r Source #

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

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

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

rFunDebug :: Monoid 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 :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b Source #

foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #

foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #

emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2 Source #

mapReft :: (r1 -> r2) -> RTypeV v c tv r1 -> RTypeV 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, ToReftV r1, Symbolic tv) => Bool -> ([Symbol] -> v1 -> m v2) -> ([Symbol] -> r1 -> m r2) -> [Symbol] -> RTypeV v1 c tv r1 -> m (RTypeV v2 c tv r2) Source #

emapRefM :: (Monad m, ToReftV t, Symbolic tv) => Bool -> ([Symbol] -> v -> m v') -> ([Symbol] -> t -> m s) -> [Symbol] -> RTPropV v c tv t -> m (RTPropV v' c tv s) Source #

mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft Source #

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

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

mapBind :: (Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV 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') -> RTypeV v c tv r -> RTypeV v' c tv r Source #

mapRTypeVM :: Monad m => (v -> m v') -> RTypeV v c tv r -> m (RTypeV 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 => Bool -> ([Symbol] -> v1 -> m v2) -> [Symbol] -> BareTypeV v1 -> m (BareTypeV v2) Source #

parsedToBareType :: BareTypeParsed -> BareType Source #

Converting To and From Sort

ofRSort :: Reftable r => RType c tv () -> RType c tv r Source #

toRSort :: RTypeV v c tv r -> RTypeV v c tv () Source #

rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source #

rTypeReft :: Reftable r => RType c tv r -> Reft Source #

stripRTypeBase :: RType c tv r -> Maybe r Source #

topRTypeBase :: Reftable 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 :: (Reftable r, TyConable c) => RType 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 :: SEnv a -> [(Symbol, a)] -> SEnv a Source #

Orphan instances

(Reftable r, TyConable c) => Subable (RTProp c tv r) Source #
Instance details Methods syms :: RTProp c tv r -> [Symbol] # substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r # substf :: (Symbol -> Expr) -> RTProp c tv r -> RTProp c tv r # subst :: Subst -> RTProp c tv r -> RTProp c tv r # subst1 :: RTProp c tv r -> (Symbol, Expr) -> RTProp c tv r #
(Subable r, Reftable r, TyConable c) => Subable (RType c tv r) Source #
Instance details Methods syms :: RType c tv r -> [Symbol] # substa :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r # substf :: (Symbol -> Expr) -> RType c tv r -> RType c tv r # subst :: Subst -> RType c tv r -> RType c tv r # subst1 :: RType c tv r -> (Symbol, Expr) -> RType c tv r #