liquidhaskell-0.5.0.1: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.RefType

Contents

Description

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

Synopsis

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r 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

Functions for decreasing arguments

isDecreasing :: Eq a => HashSet TyCon -> [a] -> RType RTyCon a t -> Bool Source

makeNumEnv :: TyConable c => [RType c b t] -> [b] Source

Functions for manipulating Predicates

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

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

tyClasses :: RefTypable RTyCon t t1 => RType RTyCon t t1 -> [(Class, [RType RTyCon t t1])] Source

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

rEx :: [(Symbol, RType c tv r)] -> RType c tv r -> RType c tv r Source

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

generalize :: RefTypable c tv r => RType c tv r -> RType c tv r Source

normalizePds :: RefTypable c tv r => RType c tv r -> RType c tv r Source

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

subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s Source

subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s Source

subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s Source

subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s Source

dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft 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

strengthenRefTypeGen :: (RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => RType c tv r -> RType c tv r -> RType c tv r Source