Safe Haskell | None |
---|---|
Language | Haskell98 |
Refinement Types. Mostly mirroring the GHC Type definition, but with room for refinements of various sorts.
- uTop :: r -> UReft r
- uReft :: (Symbol, Refa) -> UReft Reft
- uRType :: RType c tv a -> RType c tv (UReft a)
- uRType' :: RType c tv (UReft a) -> RType c tv a
- uRTypeGen :: Reftable b => RType c tv a -> RType c tv b
- uPVar :: PVar t -> UsedPVar
- applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType
- isDecreasing :: Eq a => HashSet TyCon -> [a] -> RType RTyCon a t -> Bool
- makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> (Symbol, RType RTyCon t (UReft Reft))
- makeNumEnv :: TyConable c => [RType c b t] -> [b]
- makeLexRefa :: [Expr] -> [Expr] -> UReft Reft
- pdVar :: PVar t -> Predicate
- findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
- freeTyVars :: Eq a => RType t a t1 -> [a]
- tyClasses :: RefTypable RTyCon t t1 => RType RTyCon t t1 -> [(Class, [RType RTyCon t t1])]
- tyConName :: TyCon -> Symbol
- ofType :: Monoid r => Type -> RType RTyCon RTyVar r
- toType :: (Reftable r, PPrint r) => RRType r -> Type
- rTyVar :: TyVar -> RTyVar
- rVar :: Monoid r => TyVar -> RType c RTyVar r
- rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r
- rEx :: [(Symbol, RType c tv r)] -> RType c tv r -> RType c tv r
- symbolRTyVar :: Symbol -> RTyVar
- addTyConInfo :: (PPrint r, Reftable r) => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RRType r -> RRType r
- appRTyCon :: SubsTy RTyVar (RType c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType c RTyVar r] -> RTyCon
- typeSort :: TCEmb TyCon -> Type -> Sort
- typeUniqueSymbol :: Type -> Symbol
- strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
- generalize :: RefTypable c tv r => RType c tv r -> RType c tv r
- normalizePds :: RefTypable c tv r => RType c tv r -> RType c tv r
- subts :: SubsTy tv ty c => [(tv, ty)] -> c -> c
- subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
- subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
- subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s
- subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s
- subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s
- subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s
- dataConSymbol :: DataCon -> Symbol
- dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft
- dataConReft :: DataCon -> [Symbol] -> Reft
- classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)]
- isSizeable :: HashSet TyCon -> TyCon -> Bool
- rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft
- rTypeSort :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> Sort
- shiftVV :: SpecType -> Symbol -> SpecType
- mkDataConIdsTy :: (PPrint r, Reftable r) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)]
- mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe (Symbol -> Expr) -> TyConInfo
- strengthenRefTypeGen :: (RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => RType c tv r -> RType c tv r -> RType c tv r
- strengthenDataConType :: Symbolic t => (t, RType c a (UReft Reft)) -> (t, RType c a (UReft Reft))
Functions for lifting Reft-values to Spec-values
uRType :: RType c tv a -> RType c tv (UReft a) Source
Various functions for converting vanilla Reft
to Spec
Applying a solution to a SpecType
applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType Source
Functions for decreasing arguments
makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> (Symbol, RType RTyCon t (UReft Reft)) Source
makeNumEnv :: TyConable c => [RType c b t] -> [b] Source
Functions for manipulating Predicate
s
freeTyVars :: Eq a => RType t a t1 -> [a] Source
symbolRTyVar :: Symbol -> RTyVar Source
addTyConInfo :: (PPrint r, Reftable r) => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RRType r -> RRType r Source
appRTyCon :: SubsTy RTyVar (RType c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType c RTyVar r] -> RTyCon Source
typeUniqueSymbol :: Type -> Symbol Source
strengthen :: Reftable r => RType c tv r -> r -> RType c tv r Source
generalize :: RefTypable c tv r => RType c tv r -> RType c tv r Source
normalizePds :: RefTypable c tv r => RType c tv r -> RType c tv r Source
subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s Source
subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s Source
subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s Source
subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s Source
dataConSymbol :: DataCon -> Symbol Source
dataConReft :: DataCon -> [Symbol] -> Reft Source
classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)] Source
Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)
Manipulating Refinements in RTypes
rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft Source
mkDataConIdsTy :: (PPrint r, Reftable r) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)] Source
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe (Symbol -> Expr) -> TyConInfo Source
strengthenRefTypeGen :: (RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => RType c tv r -> RType c tv r -> RType c tv r Source