liquidhaskell-0.8.10.1: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types.RefType

Description

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

Synopsis

Documentation

data TyConMap #

Information about Type Constructors

Instances

Instances details
Qualify TyConMap # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap #

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r #

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

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

Various functions for converting vanilla Reft to Spec

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 #

Applying a solution to a SpecType

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

Functions for decreasing arguments

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

Termination Predicates ----------------------------------------------------

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

Functions for manipulating Predicates

pdVar :: PVar t -> Predicate #

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

class FreeVar a v #

Minimal complete definition

freeVars

Instances

Instances details
FreeVar RTyCon RTyVar # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

FreeVar BTyCon BTyVar # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

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 #

Quantifying RTypes

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 #

RType constructors

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 #

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

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 #

Substitutions

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

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

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 #

Destructors

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]) #

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 the RTyCon as with family instances, you need BOTH the TyCon and the args to determine the extra info.

We do so in TyConMap, and by crucially extending

RefType.appRTyCon whose job is to use the Refined TyCon that is, the RTyCon generated from the TyConP to strengthen individual occurrences of the TyCon applied to various arguments.

typeUniqueSymbol :: Type -> Symbol #

classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)] #

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

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

famInstTyConType :: TyCon -> Maybe Type #

famInstArgs :: TyCon -> Maybe (TyCon, [Type]) #

famInstArgs c destructs a family-instance TyCon into its components, e.g. e.g. 'famInstArgs R:FieldBlob' is (Field, [Blob])

Manipulating Refinements in RTypes

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 #

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 #

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

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

shiftVV :: (TyConable c, Reftable (f Reft), Functor f) => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft) #

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 #

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 #

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

data Positions a #

Constructors

Pos 

Fields

Instances

Instances details
Semigroup (Positions a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(<>) :: Positions a -> Positions a -> Positions a #

sconcat :: NonEmpty (Positions a) -> Positions a #

stimes :: Integral b => b -> Positions a -> Positions a #

Monoid (Positions a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: Positions a #

mappend :: Positions a -> Positions a -> Positions a #

mconcat :: [Positions a] -> Positions a #

isNumeric :: TCEmb TyCon -> RTyCon -> Bool #

Orphan instances

Eq RTyVar #

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

Instance details

Methods

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

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

Ord RTyVar # 
Instance details

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 #

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

Instance details

Methods

showsPrec :: Int -> RTyVar -> ShowS #

show :: RTyVar -> String #

showList :: [RTyVar] -> ShowS #

Fixpoint String # 
Instance details

Methods

toFix :: String -> Doc

simplify :: String -> String

Fixpoint Class # 
Instance details

Methods

toFix :: Class -> Doc

simplify :: Class -> Class

PPrint DataCtor # 
Instance details

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

pprintPrec :: Int -> Tidy -> DataCtor -> Doc #

PPrint DataDecl # 
Instance details

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

pprintPrec :: Int -> Tidy -> DataDecl -> Doc #

Expression Var #

Converting to Fixpoint ----------------------------------------------------

Instance details

Methods

expr :: Var -> Expr

Hashable RTyCon # 
Instance details

Methods

hashWithSalt :: Int -> RTyCon -> Int

hash :: RTyCon -> Int

Hashable RTyVar # 
Instance details

Methods

hashWithSalt :: Int -> RTyVar -> Int

hash :: RTyVar -> Int

SubsTy tv RSort Predicate # 
Instance details

Methods

subt :: (tv, RSort) -> Predicate -> Predicate #

SubsTy tv ty Sort => SubsTy tv ty Expr # 
Instance details

Methods

subt :: (tv, ty) -> Expr -> Expr #

SubsTy tv ty Expr => SubsTy tv ty Reft # 
Instance details

Methods

subt :: (tv, ty) -> Reft -> Reft #

SubsTy tv ty Symbol # 
Instance details

Methods

subt :: (tv, ty) -> Symbol -> Symbol #

SubsTy tv ty () # 
Instance details

Methods

subt :: (tv, ty) -> () -> () #

SubsTy TyVar Type SpecType # 
Instance details

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType #

SubsTy Symbol RSort Sort # 
Instance details

Methods

subt :: (Symbol, RSort) -> Sort -> Sort #

SubsTy RTyVar RSort Sort # 
Instance details

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort #

SubsTy RTyVar RSort SpecType # 
Instance details

Methods

subt :: (RTyVar, RSort) -> SpecType -> SpecType #

SubsTy RTyVar RSort PrType # 
Instance details

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType #

SubsTy RTyVar RSort RSort # 
Instance details

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort #

SubsTy RTyVar RSort RTyCon # 
Instance details

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon #

SubsTy RTyVar RTyVar SpecType # 
Instance details

Methods

subt :: (RTyVar, RTyVar) -> SpecType -> SpecType #

SubsTy BTyVar BSort BSort # 
Instance details

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort #

SubsTy BTyVar BSort BTyCon # 
Instance details

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon #

SubsTy tv ty r => SubsTy tv ty (UReft r) # 
Instance details

Methods

subt :: (tv, ty) -> UReft r -> UReft r #

SubsTy tv ty ty => SubsTy tv ty (PVar ty) # 
Instance details

Methods

subt :: (tv, ty) -> PVar ty -> PVar ty #

SubsTy tv ty ty => SubsTy tv ty (PVKind ty) # 
Instance details

Methods

subt :: (tv, ty) -> PVKind ty -> PVKind ty #

SubsTy Symbol Symbol (BRType r) # 
Instance details

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r #

(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) # 
Instance details

Methods

subt :: (tv, ty) -> (a, b) -> (a, b) #

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) # 
Instance details

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r) #

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) # 
Instance details

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r #

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar # 
Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar #

SubsTy BTyVar (RType c BTyVar ()) BTyVar # 
Instance details

Methods

subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar #

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort # 
Instance details

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort #

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) # 
Instance details

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) #

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) # 
Instance details

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) #

PPrint (UReft r) => Show (UReft r) # 
Instance details

Methods

showsPrec :: Int -> UReft r -> ShowS #

show :: UReft r -> String #

showList :: [UReft r] -> ShowS #

Subable (RRProp Reft) #

Subable Instances -----------------------------------------------------

Instance details

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

Auxiliary Stuff Used Elsewhere ---------------------------------------------

Instance details

Methods

showsPrec :: Int -> RTAlias tv ty -> ShowS #

show :: RTAlias tv ty -> String #

showList :: [RTAlias tv ty] -> ShowS #

(Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ())) => Eq (RType c tv ()) # 
Instance details

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) # 
Instance details

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) # 
Instance details

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 ()))) => Semigroup (RTProp c tv r) # 
Instance details

Methods

(<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r #

sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r #

stimes :: Integral b => b -> 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 ()))) => Semigroup (RType c tv r) # 
Instance details

Methods

(<>) :: RType c tv r -> RType c tv r -> RType c tv r #

sconcat :: NonEmpty (RType c tv r) -> RType c tv r #

stimes :: Integral b => b -> RType c tv r -> RType c tv r #

(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) # 
Instance details

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) # 
Instance details

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 ()) # 
Instance details

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) # 
Instance details

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)) # 
Instance details

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 ()) # 
Instance details

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)) # 
Instance details

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

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

Instance details

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)) # 
Instance details

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]