liquidtypes-0.1: Liquid Types for Haskell

Safe HaskellSafe-Infered

Language.Haskell.Liquid.RefType

Contents

Description

Refinement Types. Mostly mirroring the GHC Type definition, but with room for refinements of various sorts.

Synopsis

Documentation

data RType p c tv r Source

Constructors

RVar 

Fields

rt_var :: !tv
 
rt_reft :: !r
 
RFun 

Fields

rt_bind :: !Symbol
 
rt_in :: !(RType p c tv r)
 
rt_out :: !(RType p c tv r)
 
rt_reft :: !r
 
RAllT 

Fields

rt_tvbind :: !tv
 
rt_ty :: !(RType p c tv r)
 
RAllP 

Fields

rt_pvbind :: !(PVar (RType p c tv ()))
 
rt_ty :: !(RType p c tv r)
 
RApp 

Fields

rt_tycon :: !c
 
rt_args :: ![RType p c tv r]
 
rt_pargs :: ![Ref r (RType p c tv r)]
 
rt_reft :: !r
 
RCls 

Fields

rt_class :: !p
 
rt_args :: ![RType p c tv r]
 
REx 

Fields

rt_bind :: !Symbol
 
rt_exarg :: !(RType p c tv r)
 
rt_ty :: !(RType p c tv r)
 
RExprArg Expr

For expression arguments to type aliases see testsposvector2.hs

ROth !String 

Instances

NFData PrType 
Inputable BareType 
Freshable RefType 
SubsTy String BSort String 
SubsTy String BSort BSort 
SubsTy RTyVar RTyVar SpecType 
SubsTy RTyVar RSort RTyCon 
SubsTy RTyVar RSort SpecType 
SubsTy RTyVar RSort PrType 
SubsTy RTyVar RSort RSort 
SubsTy tv ty (UReft r) => SubsTy tv ty (Ref (UReft r) (RType p c tv (UReft r))) 
(Monoid r, Reftable r, RefTypable a b c r) => Monoid (Ref r (RType a b c r)) 
(SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, Reftable r, RefTypable p c tv (), RefTypable p c tv (UReft r)) => Monoid (Ref r (RType p c tv (UReft r))) 
(Reftable r, RefTypable p c tv r) => Subable (Ref r (RType p c tv r)) 
Subable (Ref Reft RefType) 
(Reftable r, RefTypable p c tv r) => Reftable (Ref r (RType p c tv r)) 
Inputable (Measure BareType Symbol) 
Inputable (Spec BareType Symbol) 
Functor (RType a b c) 
RefTypable p c tv () => Eq (RType p c tv ()) 
Outputable (RType p c tv r) => Show (RType p c tv r) 
(SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, RefTypable p c tv (), RefTypable p c tv r) => Monoid (RType p c tv r) 
(NFData a, NFData b, NFData c, NFData e) => NFData (RType a b c e) 
RefTypable p c tv r => Outputable (RType p c tv r) 
(Subable r, RefTypable p c tv r) => Subable (RType p c tv r) 
Reftable r => Reftable (RType Class RTyCon RTyVar r) 

class Eq c => TyConable c whereSource

Methods

isList :: c -> BoolSource

isTuple :: c -> BoolSource

ppTycon :: c -> SDocSource

class (Monoid r, Subable r, Outputable r) => Reftable r whereSource

Methods

isTauto :: r -> BoolSource

ppTy :: r -> SDoc -> SDocSource

top :: rSource

meet :: r -> r -> rSource

toReft :: r -> ReftSource

paramsSource

Arguments

:: r 
-> [Symbol]

parameters for Reft, vv + others

fSymsSource

Arguments

:: r 
-> [Symbol]

Niki: what is this fSymsadddrop for?

addSyms :: [Symbol] -> r -> rSource

dropSyms :: r -> rSource

class (Outputable p, TyConable c, Eq p, Eq c, Eq tv, Hashable tv, Outputable tv, Reftable r) => RefTypable p c tv r whereSource

Methods

ppCls :: p -> [RType p c tv r] -> SDocSource

ppRType :: Prec -> RType p c tv r -> SDocSource

class SubsTy tv ty a whereSource

Methods

subt :: (tv, ty) -> a -> aSource

data Ref s m Source

Constructors

RMono s 
RPoly m 

Instances

SubsTy tv ty (UReft r) => SubsTy tv ty (Ref (UReft r) (RType p c tv (UReft r))) 
(Monoid r, Reftable r, RefTypable a b c r) => Monoid (Ref r (RType a b c r)) 
(SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, Reftable r, RefTypable p c tv (), RefTypable p c tv (UReft r)) => Monoid (Ref r (RType p c tv (UReft r))) 
(NFData a, NFData b) => NFData (Ref a b) 
(Reftable s, Outputable p) => Outputable (Ref s p) 
(Reftable r, RefTypable p c tv r) => Subable (Ref r (RType p c tv r)) 
Subable (Ref Reft RefType) 
(Reftable r, RefTypable p c tv r) => Reftable (Ref r (RType p c tv r)) 

data RTAlias tv ty Source

Refinement Type Aliases

Constructors

RTA 

Fields

rtName :: String
 
rtTArgs :: [tv]
 
rtVArgs :: [tv]
 
rtBody :: ty
 

Instances

(Show tv, Show ty) => Show (RTAlias tv ty) 

data PVar t Source

Predicate Variables -------------------------------------------

Constructors

PV 

Fields

pname :: !Symbol
 
ptype :: !t
 
pargs :: ![(t, Symbol, Expr)]
 

Instances

Functor PVar 
Subable UsedPVar 
SubsTy tv ty ty => SubsTy tv ty (PVar ty) 
Eq (PVar t) 
Ord (PVar t) 
Show t => Show (PVar t) 
NFData a => NFData (PVar a) 
Outputable (PVar t) 
Hashable (PVar a) 

data UReft r Source

Constructors

U 

Fields

ur_reft :: !r
 
ur_pred :: !Predicate
 

Instances

Functor UReft 
Inputable BareType 
Freshable RReft 
SubsTy RTyVar RTyVar SpecType 
SubsTy RTyVar RSort SpecType 
SubsTy tv ty (UReft r) => SubsTy tv ty (Ref (UReft r) (RType p c tv (UReft r))) 
Outputable (UReft r) => Show (UReft r) 
Monoid a => Monoid (UReft a) 
NFData r => NFData (UReft r) 
Reftable r => Outputable (UReft r) 
Subable r => Subable (UReft r) 
Reftable r => Reftable (UReft r) 
(SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, Reftable r, RefTypable p c tv (), RefTypable p c tv (UReft r)) => Monoid (Ref r (RType p c tv (UReft r))) 
Inputable (Measure BareType Symbol) 
Inputable (Spec BareType Symbol) 

data DataDecl Source

Data type refinements

Constructors

D 

Fields

tycName :: String

Type Constructor Name

tycTyVars :: [String]

Tyvar Parameters

tycPVars :: [PVar BSort]

PVar Parameters

tycDCons :: [(String, [(String, BareType)])]
DataCon, [(fieldName, fieldType)
]

Instances

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft rSource

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

Various functions for converting vanilla Reft to Spec

uRType' :: RType p c tv (UReft a) -> RType p c tv aSource

uRTypeGen :: Reftable b => RType p c tv a -> RType p c tv bSource

Functions for manipulating Predicates

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

Traversing RType

ppr_rtypeSource

Arguments

:: (RefTypable p c tv (), RefTypable p c tv r) 
=> Bool

Whether to print reftPs or not e.g. [a]...

-> Prec 
-> RType p c tv r 
-> SDoc 

efoldReft :: Reftable r => (RType p c tv r -> a) -> (SEnv a -> Maybe (RType p c tv r) -> r -> c1 -> c1) -> SEnv a -> c1 -> RType p c tv r -> c1Source

foldReft :: Reftable r => (r -> c1 -> c1) -> c1 -> RType p c tv r -> c1Source

mapReft :: (r1 -> r2) -> RType p c tv r1 -> RType p c tv r2Source

mapReftM :: Monad m => (r1 -> m r2) -> RType p c tv r1 -> m (RType p c tv r2)Source

mapBot :: (RType p c tv s -> RType p c tv s) -> RType p c tv s -> RType p c tv sSource

mapBind :: (Symbol -> Symbol) -> RType p c tv r -> RType p c tv rSource

freeTyVars :: RefTypable t t1 a t2 => RType t t1 a t2 -> [a]Source

tyClasses :: RefTypable t3 t t1 t2 => RType t3 t t1 t2 -> [(t3, [RType t3 t t1 t2])]Source

rApp :: TyCon -> [RType p RTyCon tv r] -> [Ref r (RType p RTyCon tv r)] -> r -> RType p RTyCon tv rSource

rFun :: Reftable r => Symbol -> RType p c tv r -> RType p c tv r -> RType p c tv rSource

strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv rSource

mkArrow :: Reftable r => [a] -> [PVar (RType p c a ())] -> [(Symbol, RType p c a r)] -> RType p c a r -> RType p c a rSource

mkUnivs :: [a] -> [PVar (RType p c a ())] -> RType p c a r -> RType p c a rSource

bkUniv :: RType t t1 a t2 -> ([a], [PVar (RType t t1 a ())], RType t t1 a t2)Source

bkArrow :: RType t t1 t2 t3 -> ([Symbol], [RType t t1 t2 t3], RType t t1 t2 t3)Source

generalize :: RefTypable p c a r => RType p c a r -> RType p c a rSource

normalizePds :: RefTypable p c tv r => RType p c tv r -> RType p c tv rSource

subts :: SubsTy tv ty c => [(tv, ty)] -> c -> cSource

subsTyVar_meet :: (Eq a, Hashable a, SubsTy a ty c, SubsTy a ty (PVar (RType p c a ())), Reftable s) => (a, ty, RType p c a s) -> RType p c a s -> RType p c a sSource

subsTyVars_meet :: (Eq a, Hashable a, SubsTy a ty (PVar (RType p c a ())), SubsTy a ty c, Reftable s) => [(a, ty, RType p c a s)] -> RType p c a s -> RType p c a sSource

subsTyVar_nomeet :: (Eq a, Hashable a, SubsTy a ty c, SubsTy a ty (PVar (RType p c a ())), Reftable s) => (a, ty, RType p c a s) -> RType p c a s -> RType p c a sSource

subsTyVars_nomeet :: (Eq a, Hashable a, SubsTy a ty (PVar (RType p c a ())), SubsTy a ty c, Reftable s) => [(a, ty, RType p c a s)] -> RType p c a s -> RType p c a sSource

stripRTypeBase :: RType t t1 t2 a -> Maybe aSource

rTypeReft :: Reftable r => RType p c tv r -> ReftSource

ofRSort :: Reftable r => RType p c tv () -> RType p c tv rSource

toRSort :: RType p c tv r -> RType p c tv ()Source

dataConMsReft :: Reftable r => RType p c tv r -> [Symbol] -> FReftSource

fromRMono :: [Char] -> Ref t t1 -> tSource

fromRPoly :: Ref t t1 -> t1Source

idRMono :: Ref b t -> Ref b mSource

isTrivial :: Reftable r => RType p c tv r -> BoolSource