liquidhaskell-boot
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 Source #

Information about Type Constructors

Instances

Instances details
Show TyConMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> TyConMap -> ShowS #

show :: TyConMap -> String #

showList :: [TyConMap] -> ShowS #

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReftV v 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 :: IsReft b => RType c tv a -> RType c tv b Source #

uPVar :: PVarV v t -> UsedPVarV v Source #

Applying a solution to a SpecType

applySolution :: Functor f => FInfo a -> HashMap KVar (Delayed Expr) -> f SpecType -> f SpecType Source #

Functions for decreasing arguments

isDecreasing :: HashSet TyCon -> [RTyVar] -> SpecType -> Bool Source #

makeDecrType :: Symbolic a => HashSet TyCon -> Maybe (a, (Symbol, RType RTyCon t (UReft Reft))) -> Either (Symbol, RType RTyCon t (UReft Reft)) String 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

pdVar :: PVarV v t -> PredicateV v Source #

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

class FreeVar a v Source #

Minimal complete definition

freeVars

Instances

Instances details
FreeVar BTyCon BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

allTyVars :: Ord tv => RType c tv r -> [tv] Source #

allTyVars' :: Eq tv => RType c tv r -> [tv] Source #

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

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

tyConName :: TyCon -> Symbol Source #

Quantifying RTypes

quantifyRTy :: (Monoid r, Eq tv) => [RTVar tv (RTypeV v c tv NoReft)] -> RTypeV v c tv r -> RTypeV v c tv r Source #

quantifyFreeRTy :: (Monoid r, Eq tv) => RTypeV v c tv r -> RTypeV v c tv r Source #

RType constructors

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

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

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

bTyVar :: LocSymbol -> BTyVar Source #

rTyVar :: TyVar -> RTyVar Source #

rVar :: IsReft 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 #

gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType 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 #

pdVarReft :: PVar t -> UReft Reft Source #

Substitutions

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

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

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

subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft Source #

subsTyVarMeet :: (Eq tv, Hashable tv, IsReft r, TyConable c, Binder b, SubsTy tv (RTypeBV b v c tv (NoReftB b)) c, SubsTy tv (RTypeBV b v c tv (NoReftB b)) r, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)), FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTVar tv (RTypeBV b v c tv (NoReftB b)))) => (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

subsTyVarMeet' :: (Eq tv, Hashable tv, IsReft r, TyConable c, Binder b, SubsTy tv (RTypeBV b v c tv (NoReftB b)) c, SubsTy tv (RTypeBV b v c tv (NoReftB b)) r, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)), FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTVar tv (RTypeBV b v c tv (NoReftB b)))) => (tv, RTypeBV b v c tv r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

subsTyVarNoMeet :: (Eq tv, Hashable tv, IsReft r, TyConable c, Binder b, SubsTy tv (RTypeBV b v c tv (NoReftB b)) c, SubsTy tv (RTypeBV b v c tv (NoReftB b)) r, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)), FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTVar tv (RTypeBV b v c tv (NoReftB b)))) => (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

subsTyVarsNoMeet :: (Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b, SubsTy tv (RTypeBV b v c tv (NoReftB b)) c, SubsTy tv (RTypeBV b v c tv (NoReftB b)) r, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)), FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTVar tv (RTypeBV b v c tv (NoReftB b)))) => t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

subsTyVarsMeet :: (Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b, SubsTy tv (RTypeBV b v c tv (NoReftB b)) c, SubsTy tv (RTypeBV b v c tv (NoReftB b)) r, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)), FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) (RTVar tv (RTypeBV b v c tv (NoReftB b)))) => t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r Source #

Destructors

addTyConInfo :: (PPrint r, ToReft r, SubsTy RTyVar RSort r, Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol, IsReft r) => TCEmb TyCon -> TyConMap -> RRType r -> RRType r Source #

appRTyCon :: ToTypeable r => TCEmb TyCon -> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar]) Source #

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

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

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

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

famInstTyConType :: TyCon -> Maybe Type Source #

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

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 :: Meet r => RTypeBV b v c tv r -> r -> RTypeBV b v c tv r Source #

strengthenWith :: (r -> r -> r) -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r Source #

generalize :: (Eq tv, Monoid r) => RType c tv r -> RType c tv r Source #

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

dataConMsReft :: (ToReft r, ReftBind r ~ v, ReftVar r ~ v, Refreshable v) => RTypeBV v v c tv r -> [v] -> ReftBV v v Source #

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

rTypeSortedReft :: (PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol, SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) => TCEmb TyCon -> RRType r -> SortedReft Source #

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 #1476 and #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:

{- foo :: ToNat {v:_ | 0 <= v} -}

and we'd want to expand the above to

{- foo :: {v:_ | 0 v} - Nat -}

and then resolve the hole using the (GHC) type of foo.

Annotations and Solutions -------------------------------------------------

rTypeSort :: (PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol, SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) => TCEmb TyCon -> RRType r -> Sort Source #

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

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

shiftVV :: (TyConable c, IsReft (f Reft), Functor f, Subable (f Reft), Variable (f Reft) ~ Variable Reft, ReftBind (f Reft) ~ ReftBind Reft) => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft) Source #

TODO: classify these

expandProductType :: (PPrint r, IsReft r, SubsTy RTyVar (RType RTyCon RTyVar NoReft) r, ReftBind r ~ Symbol, ReftVar r ~ Symbol, Variable r ~ Symbol) => Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo Source #

strengthenRefTypeGen :: (OkRTBV v v c tv r, Subable r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => RTypeBV v v c tv r -> RTypeBV v v c tv r -> RTypeBV v v c tv r Source #

strengthenDataConType :: (Var, SpecType) -> (Var, SpecType) Source #

isBaseTy :: Type -> Bool Source #

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

isValKind :: Kind -> Bool Source #

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

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

tyVarsPosition :: RType RTyCon tv r -> Positions tv Source #

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

Constructors

Pos 

Fields

Instances

Instances details
Monoid (Positions a) Source # 
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 #

Semigroup (Positions a) Source # 
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 #

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

Orphan instances

Eq RTyVar Source #

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

Instance details

Methods

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

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

Ord RTyVar Source # 
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 #

Hashable RTyCon Source # 
Instance details

Methods

hashWithSalt :: Int -> RTyCon -> Int #

hash :: RTyCon -> Int #

Hashable RTyVar Source # 
Instance details

Methods

hashWithSalt :: Int -> RTyVar -> Int #

hash :: RTyVar -> Int #

Fixpoint Class Source # 
Instance details

Methods

toFix :: Class -> Doc

simplify :: Class -> Class

Fixpoint String Source # 
Instance details

Methods

toFix :: String -> Doc

simplify :: String -> String

Expression Var Source #

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

Instance details

Methods

expr :: Var -> Expr

SubsTy TyVar Type SpecType Source # 
Instance details

Methods

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

SubsTy Symbol RSort Sort Source # 
Instance details

Methods

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

SubsTy BTyVar BSort BSort Source # 
Instance details

Methods

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

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Methods

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

SubsTy RTyVar RSort Sort Source # 
Instance details

Methods

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

SubsTy RTyVar RSort RSort Source # 
Instance details

Methods

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

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Methods

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

SubsTy RTyVar RSort SpecType Source # 
Instance details

Methods

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

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Methods

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

SubsTy tv RSort Predicate Source # 
Instance details

Methods

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

SubsTy tv ty Symbol Source # 
Instance details

Methods

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

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

Methods

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

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

Methods

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

SubsTy tv ty NoReft Source # 
Instance details

Methods

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

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

SubsTy tv ty ty => SubsTy tv ty (PVarBV b v ty) Source # 
Instance details

Methods

subt :: (tv, ty) -> PVarBV b v ty -> PVarBV b v ty Source #

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

Subable (RRProp Reft) Source #

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

Instance details

Associated Types

type Variable (RRProp Reft) 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

type Variable (RRProp Reft) = Symbol
type Variable (RTPropBV v v c tv r) 
Instance details

Defined in Language.Haskell.Liquid.Types.RTypeOp

type Variable (RTPropBV v v c tv r) = v

Methods

syms :: RRProp Reft -> [Variable (RRProp Reft)]

substa :: (Variable (RRProp Reft) -> Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft

substf :: (Variable (RRProp Reft) -> ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft -> RRProp Reft

subst :: SubstV (Variable (RRProp Reft)) -> RRProp Reft -> RRProp Reft

subst1 :: RRProp Reft -> (Variable (RRProp Reft), ExprBV (Variable (RRProp Reft)) (Variable (RRProp Reft))) -> RRProp Reft

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

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) => Eq (RType c tv NoReft) Source # 
Instance details

Methods

(==) :: RType c tv NoReft -> RType c tv NoReft -> Bool #

(/=) :: RType c tv NoReft -> RType c tv NoReft -> Bool #

Meet (RTProp BTyCon BTyVar NoReft) Source # 
Instance details

Methods

meet :: RTProp BTyCon BTyVar NoReft -> RTProp BTyCon BTyVar NoReft -> RTProp BTyCon BTyVar NoReft Source #

Meet (RTProp BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Methods

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) Source #

Meet (RTProp RTyCon RTyVar Reft) Source # 
Instance details

Methods

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft Source #

Meet (RTProp RTyCon RTyVar NoReft) Source # 
Instance details

Methods

meet :: RTProp RTyCon RTyVar NoReft -> RTProp RTyCon RTyVar NoReft -> RTProp RTyCon RTyVar NoReft Source #

Meet (RTProp RTyCon RTyVar (UReft Reft)) Source # 
Instance details

Methods

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) Source #

Meet (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

Methods

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) Source #

Semigroup (RType RTyCon RTyVar r) => Meet (RType RTyCon RTyVar r) Source # 
Instance details

Methods

meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r Source #

(SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTPropBV v v c tv r) Source # 
Instance details

Methods

mempty :: RTPropBV v v c tv r #

mappend :: RTPropBV v v c tv r -> RTPropBV v v c tv r -> RTPropBV v v c tv r #

mconcat :: [RTPropBV v v c tv r] -> RTPropBV v v c tv r #

(SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, FreeVar c tv, Subable r, Variable r ~ v, ReftBind r ~ v, IsReft r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Monoid (RTypeBV v v c tv r) Source # 
Instance details

Methods

mempty :: RTypeBV v v c tv r #

mappend :: RTypeBV v v c tv r -> RTypeBV v v c tv r -> RTypeBV v v c tv r #

mconcat :: [RTypeBV v v c tv r] -> RTypeBV v v c tv r #

(SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTPropBV v v c tv r) Source # 
Instance details

Methods

(<>) :: RTPropBV v v c tv r -> RTPropBV v v c tv r -> RTPropBV v v c tv r #

sconcat :: NonEmpty (RTPropBV v v c tv r) -> RTPropBV v v c tv r #

stimes :: Integral b => b -> RTPropBV v v c tv r -> RTPropBV v v c tv r #

(SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, FreeVar c tv, Subable r, Variable r ~ v, ReftBind r ~ v, IsReft r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Semigroup (RTypeBV v v c tv r) Source # 
Instance details

Methods

(<>) :: RTypeBV v v c tv r -> RTypeBV v v c tv r -> RTypeBV v v c tv r #

sconcat :: NonEmpty (RTypeBV v v c tv r) -> RTypeBV v v c tv r #

stimes :: Integral b => b -> RTypeBV v v c tv r -> RTypeBV v v c tv r #

(SubsTy tv (RTypeBV v v c tv (NoReftB v)) c, OkRTBV v v c tv r, Variable r ~ v, ReftBind r ~ v, IsReft r, FreeVar c tv, Subable r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) r, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTypeBV v v c tv (NoReftB v)), SubsTy tv (RTypeBV v v c tv (NoReftB v)) tv, SubsTy tv (RTypeBV v v c tv (NoReftB v)) (RTVar tv (RTypeBV v v c tv (NoReftB v)))) => Meet (RTPropBV v v c tv r) Source # 
Instance details

Methods

meet :: RTPropBV v v c tv r -> RTPropBV v v c tv r -> RTPropBV v v c tv r Source #