liquidhaskell-0.8.0.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types.RefType

Contents

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 #

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 Predicates

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

class FreeVar a v Source #

Minimal complete definition

freeVars

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

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

bTyVar :: Symbol -> BTyVar 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 #

Substitutions

subts :: (Foldable t, SubsTy tv ty c) => t (tv, ty) -> c -> c Source #

Type Substitutions --------------------------------------------------------

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 #

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

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

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 #

Orphan instances

Eq RTyVar Source # 

Methods

(==) :: RTyVar -> RTyVar -> Bool #

(/=) :: RTyVar -> RTyVar -> Bool #

Eq Predicate Source #

Wrappers for GHC Type Elements --------------------------------------------

Ord RTyCon Source # 
Ord RTyVar Source # 
Show RTyVar Source #

Printing Refinement Types -------------------------------------------------

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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
Reftable (RTProp BTyCon BTyVar ()) Source # 
Reftable (RTProp BTyCon BTyVar (UReft Reft)) Source # 
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r) Source #

Reftable Instances -------------------------------------------------------

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]