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.
Synopsis
- data TyConMap
- 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 :: HashSet TyCon -> [RTyVar] -> SpecType -> Bool
- makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> Either (Symbol, RType RTyCon t (UReft Reft)) String
- 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
- allTyVars :: Ord tv => RType c tv r -> [tv]
- 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 :: (Monoid r, Eq tv) => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
- quantifyFreeRTy :: (Monoid r, 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
- gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType
- 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
- pdVarReft :: PVar t -> UReft Reft
- subts :: SubsTy tv ty c => [(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)) => TCEmb TyCon -> TyConMap -> RRType r -> RRType r
- appRTyCon :: ToTypeable r => TCEmb TyCon -> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
- typeUniqueSymbol :: Type -> Symbol
- classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
- isSizeable :: HashSet TyCon -> TyCon -> Bool
- famInstTyConType :: TyCon -> Maybe Type
- famInstArgs :: TyCon -> Maybe (TyCon, [Type])
- strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
- generalize :: (Eq tv, Monoid r) => 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 :: (TyConable c, Reftable (f Reft), Functor f) => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
- expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
- mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
- 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 :: (Var, SpecType) -> (Var, SpecType)
- 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)
- tyVarsPosition :: RType RTyCon tv r -> Positions tv
- data Positions a = Pos {}
- isNumeric :: TCEmb TyCon -> RTyCon -> Bool
Documentation
Information about Type Constructors
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)))] -> Either (Symbol, RType RTyCon t (UReft Reft)) String Source #
makeNumEnv :: (Foldable t, TyConable c) => t (RType c b t1) -> [b] Source #
Termination Predicates ----------------------------------------------------
Functions for manipulating Predicate
s
freeVars
Quantifying RTypes
quantifyRTy :: (Monoid r, Eq tv) => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r Source #
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 :: SubsTy tv ty c => [(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)) => TCEmb TyCon -> TyConMap -> RRType r -> RRType r Source #
appRTyCon :: ToTypeable r => TCEmb TyCon -> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar]) Source #
- NOTE:FamInstPredVars
- related to [NOTE:FamInstEmbeds]
See testsdataconpos/T1446.hs
The function txRefSort converts
Intp ===> {v:Int | p v}
which is fine, but also converts
Fieldq Blob a ===> {v:Field Blob a | q v}
which is NOT ok, because q expects a different arg.
The above happens because, thanks to instance-family stuff, LH doesn't realize that q is actually an ARG of Field Blob Note that Field itself has no args, but Field Blob does...
That is, it is not enough to store the refined
TyCon
info, solely in theRTyCon
as with family instances, you need BOTH theTyCon
and the args to determine the extra info.We do so in
TyConMap
, and by crucially extendingRefType.appRTyCon
whose job is to use the RefinedTyCon
that is, theRTyCon
generated from theTyConP
to strengthen individual occurrences of the TyCon applied to various arguments.
typeUniqueSymbol :: Type -> Symbol Source #
classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)] Source #
Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)
famInstArgs :: TyCon -> Maybe (TyCon, [Type]) Source #
famInstArgs c
destructs a family-instance TyCon
into its components, e.g.
e.g. 'famInstArgs R:FieldBlob' is (Field, [Blob])
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 #
- NOTE:Hole-Lit
We use toType
to convert RType to GHC.Type to expand any GHC
related type-aliases, e.g. in Bare.Resolve.expandRTypeSynonyms.
If the RType has a RHole then what to do?
We, encode RHole
as `LitTy LH_HOLE` -- which is a bit of
a *hack*. The only saving grace is it is used *temporarily*
and then swiftly turned back into an RHole
via ofType
(after GHC has done its business of expansion).
Of course, we hope this doesn't break any GHC invariants! See issue 1477
The other option is to *not* use toType
on things that have
holes in them, but this seems worse, e.g. because you may define
a plain GHC alias like:
type ToNat a = a -> Nat
and then you might write refinement types like:
and we'd want to expand the above to
and then resolve the hole using the (GHC) type of foo
.
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 #
typeSort :: TCEmb TyCon -> Type -> Sort Source #
From Old Fixpoint ---------------------------------------------------------
shiftVV :: (TyConable c, Reftable (f Reft), Functor f) => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft) Source #
TODO: classify these
expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Var -> RType RTyCon RTyVar r -> 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 #
tyVarsPosition :: RType RTyCon tv r -> Positions tv Source #
tyVarsPosition t returns the type variables appearing | (in positive positions, in negative positions, in undetermined positions) | undetermined positions are due to type constructors and type application