Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.RefType

Contents

Functions for lifting Reft-values to Spec-values
Applying a solution to a SpecType
Functions for decreasing arguments
Functions for manipulating Predicates
Quantifying RTypes
RType constructors
Substitutions
Destructors
Manipulating Refinements in RTypes
TODO: classify these
Orphan instances

Description

Refinement Types. Mostly mirroring the GHC Type definition, but with room for refinements of various sorts. TODO: Desperately needs re-organization.

Synopsis

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r Source #

uReft :: (Symbol, Expr) -> UReft Reft Source #

uRType :: RType c tv a -> RType c tv (UReft a) Source #

Various functions for converting vanilla Reft to Spec

uRType' :: RType c tv (UReft a) -> RType c tv a Source #

uRTypeGen :: Reftable b => RType c tv a -> RType c tv b Source #

uPVar :: PVar t -> UsedPVar Source #

Applying a solution to a SpecType

applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType Source #

Functions for decreasing arguments

isDecreasing :: (Eq a, Foldable t1) => HashSet TyCon -> t1 a -> RType RTyCon a t -> Bool Source #

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 ----------------------------------------------------

makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft Source #

Functions for manipulating `Predicate`s

pdVar :: PVar t -> Predicate Source #

findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ()) Source #

class FreeVar a v Source #

Minimal complete definition

freeVars

Instances

FreeVar RTyCon RTyVar Source #
Methods freeVars :: RTyCon -> [RTyVar]
FreeVar BTyCon BTyVar Source #
Methods freeVars :: BTyCon -> [BTyVar]

freeTyVars :: Eq tv => RType c tv r -> [RTVar tv (RType c tv ())] Source #

tyClasses :: OkRT RTyCon tv r => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])] Source #

tyConName :: TyCon -> Symbol Source #

Quantifying RTypes

quantifyRTy :: Eq tv => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r Source #

quantifyFreeRTy :: Eq tv => RType c tv r -> RType c tv r Source #

RType constructors

ofType :: Monoid r => Type -> RRType r Source #

toType :: ToTypeable r => RRType r -> Type Source #

bareOfType :: Monoid r => Type -> BRType r Source #

bTyVar :: Symbol -> BTyVar Source #

rTyVar :: TyVar -> RTyVar Source #

rVar :: Monoid r => TyVar -> RType c RTyVar r Source #

Helper Functions (RJ: Helping to do what?) --------------------------------

rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r Source #

rEx :: Foldable t => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r Source #

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 --------------------------------------------------------

subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate Source #

subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft 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 (), 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 #

classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)] Source #

Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)

isSizeable :: HashSet TyCon -> TyCon -> Bool Source #

Manipulating Refinements in RTypes

strengthen :: Reftable r => RType c tv r -> r -> RType c tv r Source #

generalize :: Eq tv => RType c tv r -> RType c tv r Source #

normalizePds :: OkRT c tv r => RType c tv r -> RType c tv r Source #

dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft Source #

dataConReft :: DataCon -> [Symbol] -> Reft Source #

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 #

typeSort :: TCEmb TyCon -> Type -> Sort Source #

From Old Fixpoint ---------------------------------------------------------

shiftVV :: SpecType -> Symbol -> SpecType 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 #

meetable :: OkRT c tv r => RType c tv r -> RType c tv r -> Bool 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 #

isBaseTy :: Type -> Bool Source #

updateRTVar :: Monoid r => RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r) Source #

isValKind :: Kind -> Bool Source #

kindToRType :: Monoid r => Type -> RRType r Source #

rTVarInfo :: Monoid r => TyVar -> RTVInfo (RRType r) Source #

Orphan instances

Eq RTyVar Source #
Methods (==) :: RTyVar -> RTyVar -> Bool # (/=) :: RTyVar -> RTyVar -> Bool #
Eq Predicate Source #	Wrappers for GHC Type Elements --------------------------------------------
Methods (==) :: Predicate -> Predicate -> Bool # (/=) :: Predicate -> Predicate -> Bool #
Ord RTyCon Source #
Methods compare :: RTyCon -> RTyCon -> Ordering # (<) :: RTyCon -> RTyCon -> Bool # (<=) :: RTyCon -> RTyCon -> Bool # (>) :: RTyCon -> RTyCon -> Bool # (>=) :: RTyCon -> RTyCon -> Bool # max :: RTyCon -> RTyCon -> RTyCon # min :: RTyCon -> RTyCon -> RTyCon #
Ord RTyVar Source #
Methods compare :: RTyVar -> RTyVar -> Ordering # (<) :: RTyVar -> RTyVar -> Bool # (<=) :: RTyVar -> RTyVar -> Bool # (>) :: RTyVar -> RTyVar -> Bool # (>=) :: RTyVar -> RTyVar -> Bool # max :: RTyVar -> RTyVar -> RTyVar # min :: RTyVar -> RTyVar -> RTyVar #
Show RTyVar Source #	Printing Refinement Types -------------------------------------------------
Methods showsPrec :: Int -> RTyVar -> ShowS # show :: RTyVar -> String # showList :: [RTyVar] -> ShowS #
Hashable RTyCon Source #
Methods hashWithSalt :: Int -> RTyCon -> Int # hash :: RTyCon -> Int #
Hashable RTyVar Source #
Methods hashWithSalt :: Int -> RTyVar -> Int # hash :: RTyVar -> Int #
Expression Var Source #	Converting to Fixpoint ----------------------------------------------------
Methods expr :: Var -> Expr
PPrint REnv Source #
Methods pprintTidy :: Tidy -> REnv -> Doc # pprintPrec :: Int -> Tidy -> REnv -> Doc #
PPrint DataCtor Source #
Methods pprintTidy :: Tidy -> DataCtor -> Doc # pprintPrec :: Int -> Tidy -> DataCtor -> Doc #
Fixpoint String Source #
Methods toFix :: String -> Doc simplify :: String -> String
Fixpoint Class Source #
Methods toFix :: Class -> Doc simplify :: Class -> Class
SubsTy tv RSort Predicate Source #
Methods subt :: (tv, RSort) -> Predicate -> Predicate Source #
SubsTy tv ty Sort => SubsTy tv ty Expr Source #
Methods subt :: (tv, ty) -> Expr -> Expr Source #
SubsTy tv ty Expr => SubsTy tv ty Reft Source #
Methods subt :: (tv, ty) -> Reft -> Reft Source #
SubsTy tv ty Symbol Source #
Methods subt :: (tv, ty) -> Symbol -> Symbol Source #
SubsTy tv ty () Source #
Methods subt :: (tv, ty) -> () -> () Source #
SubsTy TyVar Type SpecType Source #
Methods subt :: (TyVar, Type) -> SpecType -> SpecType Source #
SubsTy Symbol RSort Sort Source #
Methods subt :: (Symbol, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort Sort Source #
Methods subt :: (RTyVar, RSort) -> Sort -> Sort Source #
SubsTy RTyVar RSort SpecType Source #
Methods subt :: (RTyVar, RSort) -> SpecType -> SpecType Source #
SubsTy RTyVar RSort PrType Source #
Methods subt :: (RTyVar, RSort) -> PrType -> PrType Source #
SubsTy RTyVar RSort RSort Source #
Methods subt :: (RTyVar, RSort) -> RSort -> RSort Source #
SubsTy RTyVar RSort RTyCon Source #
Methods subt :: (RTyVar, RSort) -> RTyCon -> RTyCon Source #
SubsTy RTyVar RTyVar SpecType Source #
Methods subt :: (RTyVar, RTyVar) -> SpecType -> SpecType Source #
SubsTy BTyVar BSort BSort Source #
Methods subt :: (BTyVar, BSort) -> BSort -> BSort Source #
SubsTy BTyVar BSort BTyCon Source #
Methods subt :: (BTyVar, BSort) -> BTyCon -> BTyCon Source #
SubsTy tv ty r => SubsTy tv ty (UReft r) Source #
Methods subt :: (tv, ty) -> UReft r -> UReft r Source #
SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source #
Methods subt :: (tv, ty) -> PVar ty -> PVar ty Source #
SubsTy tv ty ty => SubsTy tv ty (PVKind ty) Source #
Methods subt :: (tv, ty) -> PVKind ty -> PVKind ty Source #
(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) Source #
Methods subt :: (tv, ty) -> (a, b) -> (a, b) Source #
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source #
Methods subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source #
Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar Source #
SubsTy BTyVar (RType c BTyVar ()) BTyVar Source #
Methods subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar Source #
SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source #
Methods subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort Source #
SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source #
Methods subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) Source #
SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source #
Methods subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) Source #
PPrint (UReft r) => Show (UReft r) Source #
Methods showsPrec :: Int -> UReft r -> ShowS # show :: UReft r -> String # showList :: [UReft r] -> ShowS #
Subable (RRProp Reft) Source #	Subable Instances -----------------------------------------------------
Methods syms :: RRProp Reft -> [Symbol] substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft subst :: Subst -> RRProp Reft -> RRProp Reft subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft
(Show tv, Show ty) => Show (RTAlias tv ty) Source #	Auxiliary Stuff Used Elsewhere ---------------------------------------------
Methods showsPrec :: Int -> RTAlias tv ty -> ShowS # show :: RTAlias tv ty -> String # showList :: [RTAlias tv ty] -> ShowS #
(Eq c, Eq tv, Hashable tv) => Eq (RType c tv ()) Source #
Methods (==) :: RType c tv () -> RType c tv () -> Bool # (/=) :: RType c tv () -> RType c tv () -> Bool #
PPrint (RTProp c tv r) => Show (RTProp c tv r) Source #
Methods showsPrec :: Int -> RTProp c tv r -> ShowS # show :: RTProp c tv r -> String # showList :: [RTProp c tv r] -> ShowS #
PPrint (RType c tv r) => Show (RType c tv r) Source #
Methods showsPrec :: Int -> RType c tv r -> ShowS # show :: RType c tv r -> String # showList :: [RType c tv r] -> ShowS #
(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r) Source #
Methods mempty :: RTProp c tv r # mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r # mconcat :: [RTProp c tv r] -> RTProp c tv r #
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RType c tv r) Source #
Methods mempty :: RType c tv r # mappend :: RType c tv r -> RType c tv r -> RType c tv r # mconcat :: [RType c tv r] -> RType c tv r #
Reftable (RTProp RTyCon RTyVar ()) Source #
Methods isTauto :: RTProp RTyCon RTyVar () -> Bool ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () toReft :: RTProp RTyCon RTyVar () -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar () params :: RTProp RTyCon RTyVar () -> [Symbol]
Reftable (RTProp RTyCon RTyVar Reft) Source #
Methods isTauto :: RTProp RTyCon RTyVar Reft -> Bool ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft toReft :: RTProp RTyCon RTyVar Reft -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar Reft params :: RTProp RTyCon RTyVar Reft -> [Symbol]
Reftable (RTProp RTyCon RTyVar (UReft Reft)) Source #
Methods isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft) params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
Reftable (RTProp BTyCon BTyVar ()) Source #
Methods isTauto :: RTProp BTyCon BTyVar () -> Bool ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () toReft :: RTProp BTyCon BTyVar () -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar () params :: RTProp BTyCon BTyVar () -> [Symbol]
Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source #
Methods isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft) params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r) Source #	Reftable Instances -------------------------------------------------------
Methods isTauto :: RType RTyCon RTyVar r -> Bool ppTy :: RType RTyCon RTyVar r -> Doc -> Doc top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r toReft :: RType RTyCon RTyVar r -> Reft ofReft :: Reft -> RType RTyCon RTyVar r params :: RType RTyCon RTyVar r -> [Symbol]
Reftable (RType BTyCon BTyVar (UReft Reft)) Source #
Methods isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft) params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]