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 p c tv a -> RType p c tv (UReft a)
- uRType' :: RType p c tv (UReft a) -> RType p c tv a
- uRTypeGen :: Reftable b => RType p c tv a -> RType p c tv b
- uPVar :: PVar t -> UsedPVar
- applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType
- isDecreasing :: RType t RTyCon t1 t2 -> Bool
- makeDecrType :: Symbolic a => [(a, (Symbol, RType p RTyCon tv (UReft Reft)))] -> (Symbol, RType p RTyCon tv (UReft Reft))
- makeLexRefa :: [Expr] -> [Expr] -> UReft Reft
- pdVar :: PVar t -> Predicate
- findPVar :: [PVar (RType p c tv ())] -> UsedPVar -> PVar (RType p c tv ())
- freeTyVars :: RefTypable t t1 a t2 => RType t t1 a t2 -> [a]
- tyClasses :: RefTypable t RTyCon t1 t2 => RType t RTyCon t1 t2 -> [(Class, [RType t RTyCon t1 t2])]
- tyConName :: TyCon -> Symbol
- ofType :: Monoid r => Type -> RType p RTyCon RTyVar r
- toType :: (Reftable r, PPrint r) => RRType r -> Type
- rTyVar :: TyVar -> RTyVar
- rVar :: Monoid r => TyVar -> RType p c RTyVar r
- rApp :: TyCon -> [RType p RTyCon tv r] -> [RTProp p RTyCon tv r] -> r -> RType p RTyCon tv r
- rEx :: [(Symbol, RType p c tv r)] -> RType p c tv r -> RType p c tv r
- addTyConInfo :: (PPrint r, Reftable r) => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RRType r -> RRType r
- appRTyCon :: SubsTy RTyVar (RType p c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType p c RTyVar r] -> RTyCon
- typeSort :: TCEmb TyCon -> Type -> Sort
- typeUniqueSymbol :: Type -> Symbol
- strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv r
- generalize :: RefTypable c p tv r => RType c p tv r -> RType c p tv r
- normalizePds :: RefTypable p c tv r => RType p c tv r -> RType p 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 p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s
- subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s
- subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s
- subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s
- dataConSymbol :: DataCon -> Symbol
- dataConMsReft :: Reftable r => RType p c tv r -> [Symbol] -> Reft
- dataConReft :: DataCon -> [Symbol] -> Reft
- literalFRefType :: TCEmb TyCon -> Literal -> RType p RTyCon RTyVar Reft
- literalFReft :: TCEmb TyCon -> Literal -> Reft
- literalConst :: TCEmb TyCon -> Literal -> (Sort, Maybe Expr)
- classBinds :: TyConable c => RType t c RTyVar t1 -> [(Symbol, SortedReft)]
- 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 Class RTyCon RTyVar r) -> [(Var, RType Class RTyCon RTyVar r)]
- mkTyConInfo :: TyCon -> [Int] -> [Int] -> Maybe (Symbol -> Expr) -> TyConInfo
Functions for lifting Reft-values to Spec-values
uRType :: RType p c tv a -> RType p 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
isDecreasing :: RType t RTyCon t1 t2 -> Bool Source
makeDecrType :: Symbolic a => [(a, (Symbol, RType p RTyCon tv (UReft Reft)))] -> (Symbol, RType p RTyCon tv (UReft Reft)) Source
Functions for manipulating Predicate
s
freeTyVars :: RefTypable t t1 a t2 => RType t t1 a t2 -> [a] Source
tyClasses :: RefTypable t RTyCon t1 t2 => RType t RTyCon t1 t2 -> [(Class, [RType t RTyCon t1 t2])] Source
addTyConInfo :: (PPrint r, Reftable r) => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RRType r -> RRType r Source
appRTyCon :: SubsTy RTyVar (RType p c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType p c RTyVar r] -> RTyCon Source
typeUniqueSymbol :: Type -> Symbol Source
strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv r Source
generalize :: RefTypable c p tv r => RType c p tv r -> RType c p tv r Source
normalizePds :: RefTypable p c tv r => RType p c tv r -> RType p c tv r Source
subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s Source
subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s Source
subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s Source
subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s Source
dataConSymbol :: DataCon -> Symbol Source
dataConReft :: DataCon -> [Symbol] -> Reft Source
literalConst :: TCEmb TyCon -> Literal -> (Sort, Maybe Expr) Source
literalConst
returns Nothing
for unhandled lits because
otherwise string-literals show up as global int-constants
which blow up qualifier instantiation.
classBinds :: TyConable c => RType t c RTyVar t1 -> [(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