Safe Haskell | None |
---|---|
Language | Haskell98 |
Refinement Types. Mostly mirroring the GHC Type definition, but with room for refinements of various sorts. TODO: Desperately needs re-organization.
- uTop :: r -> UReft r
- uReft :: (Symbol, Expr) -> 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, Foldable t1) => HashSet TyCon -> t1 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 :: (Foldable t, TyConable c) => t (RType c b t1) -> [b]
- makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft
- pdVar :: PVar t -> Predicate
- findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
- class FreeVar a v
- freeTyVars :: Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
- tyClasses :: OkRT RTyCon tv r => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
- tyConName :: TyCon -> Symbol
- quantifyRTy :: Eq tv => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
- quantifyFreeRTy :: Eq tv => RType c tv r -> RType c tv r
- ofType :: Monoid r => Type -> RRType r
- toType :: ToTypeable r => RRType r -> Type
- bareOfType :: Monoid r => Type -> BRType r
- bTyVar :: Symbol -> BTyVar
- 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 :: Foldable t => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
- symbolRTyVar :: Symbol -> RTyVar
- bareRTyVar :: BTyVar -> RTyVar
- tyConBTyCon :: TyCon -> BTyCon
- subts :: (Foldable t, SubsTy tv ty c) => t (tv, ty) -> c -> c
- subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
- subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
- subsTyVar_meet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
- subsTyVar_meet' :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv r) -> RType c tv r -> RType c tv r
- subsTyVar_nomeet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
- subsTyVars_nomeet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
- subsTyVars_meet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
- addTyConInfo :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar 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
- typeUniqueSymbol :: Type -> Symbol
- classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)]
- isSizeable :: HashSet TyCon -> TyCon -> Bool
- strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
- generalize :: Eq tv => RType c tv r -> RType c tv r
- normalizePds :: OkRT c tv r => RType c tv r -> RType c tv r
- dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft
- dataConReft :: DataCon -> [Symbol] -> Reft
- rTypeSortedReft :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> SortedReft
- rTypeSort :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> Sort
- typeSort :: TCEmb TyCon -> Type -> Sort
- shiftVV :: SpecType -> Symbol -> SpecType
- mkDataConIdsTy :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)]
- mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
- meetable :: OkRT c tv r => RType c tv r -> RType c tv r -> Bool
- strengthenRefTypeGen :: (OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => RType c tv r -> RType c tv r -> RType c tv r
- strengthenDataConType :: Symbolic t => (t, RType c tv (UReft Reft)) -> (t, RType c tv (UReft Reft))
- isBaseTy :: Type -> Bool
- updateRTVar :: Monoid r => RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
- isValKind :: Kind -> Bool
- kindToRType :: Monoid r => Type -> RRType r
- rTVarInfo :: Monoid r => TyVar -> RTVInfo (RRType r)
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 :: (Foldable t, TyConable c) => t (RType c b t1) -> [b] Source #
Termination Predicates ----------------------------------------------------
Functions for manipulating Predicate
s
Quantifying RTypes
RType constructors
rVar :: Monoid r => TyVar -> RType c RTyVar r Source #
Helper Functions (RJ: Helping to do what?) --------------------------------
symbolRTyVar :: Symbol -> RTyVar Source #
bareRTyVar :: BTyVar -> RTyVar Source #
tyConBTyCon :: TyCon -> BTyCon Source #
Substitutions
subts :: (Foldable t, SubsTy tv ty c) => t (tv, ty) -> c -> c Source #
Type Substitutions --------------------------------------------------------
subsTyVar_meet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r Source #
subsTyVar_meet' :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv r) -> RType c tv r -> RType c tv r Source #
subsTyVar_nomeet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r Source #
subsTyVars_nomeet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r Source #
subsTyVars_meet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r Source #
Destructors
addTyConInfo :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar 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 #
From Old Fixpoint ---------------------------------------------------------
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, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> SortedReft Source #
Annotations and Solutions -------------------------------------------------
rTypeSort :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> Sort Source #
TODO: classify these
mkDataConIdsTy :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)] Source #
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo Source #
strengthenRefTypeGen :: (OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => RType c tv r -> RType c tv r -> RType c tv r Source #
strengthenDataConType :: Symbolic t => (t, RType c tv (UReft Reft)) -> (t, RType c tv (UReft Reft)) Source #