Language.Haskell.Liquid.RefType

Contents

• Functions for lifting Reft-values to Spec-values
• Functions for manipulating Predicates
• Traversing RType

Description

Synopsis

• newtype RTyVar = RTV TyVar
• data RType p c tv r
  • = RVar {
    • rt_var :: !tv
    • rt_reft :: !r
    }
  • | RFun {
    • rt_bind :: !Symbol
    • rt_in :: !(RType p c tv r)
    • rt_out :: !(RType p c tv r)
    • rt_reft :: !r
    }
  • | RAllT {
    • rt_tvbind :: !tv
    • rt_ty :: !(RType p c tv r)
    }
  • | RAllP {
    • rt_pvbind :: !(PVar (RType p c tv ()))
    • rt_ty :: !(RType p c tv r)
    }
  • | RApp {
    • rt_tycon :: !c
    • rt_args :: ![RType p c tv r]
    • rt_pargs :: ![Ref r (RType p c tv r)]
    • rt_reft :: !r
    }
  • | RCls {
    • rt_class :: !p
    • rt_args :: ![RType p c tv r]
    }
  • | REx {
    • rt_bind :: !Symbol
    • rt_exarg :: !(RType p c tv r)
    • rt_ty :: !(RType p c tv r)
    }
  • | RExprArg Expr
  • | ROth !String
• type RRType = RType Class RTyCon RTyVar
• type BRType = RType String String String
• data RTyCon = RTyCon {
  • rTyCon :: !TyCon
  • rTyConPs :: ![RPVar]
  }
• class Eq c => TyConable c where
  • isList :: c -> Bool
  • isTuple :: c -> Bool
  • ppTycon :: c -> SDoc
• class (Monoid r, Subable r, Outputable r) => Reftable r where
  • isTauto :: r -> Bool
  • ppTy :: r -> SDoc -> SDoc
  • top :: r
  • meet :: r -> r -> r
  • toReft :: r -> Reft
  • params :: r -> [Symbol]
  • fSyms :: r -> [Symbol]
  • addSyms :: [Symbol] -> r -> r
  • dropSyms :: r -> r
• class (Outputable p, TyConable c, Eq p, Eq c, Eq tv, Hashable tv, Outputable tv, Reftable r) => RefTypable p c tv r where
  • ppCls :: p -> [RType p c tv r] -> SDoc
  • ppRType :: Prec -> RType p c tv r -> SDoc
• class SubsTy tv ty a where
  • subt :: (tv, ty) -> a -> a
• data Ref s m
  • = RMono s
  • | RPoly m
• data RTAlias tv ty = RTA {
  • rtName :: String
  • rtTArgs :: [tv]
  • rtVArgs :: [tv]
  • rtBody :: ty
  }
• data FReft
  • = FSReft [Symbol] Reft
  • | FReft Reft
• reft :: (Symbol, [Refa]) -> FReft
• fFReft :: (Reft -> Reft) -> FReft -> FReft
• toFReft :: Reft -> FReft
• fromFReft :: FReft -> Reft
• splitFReft :: FReft -> ([Symbol], Reft)
• type BSort = BRType ()
• type BPVar = PVar BSort
• type BareType = BRType RReft
• type RSort = RRType ()
• type UsedPVar = PVar ()
• type RPVar = PVar RSort
• type RReft = UReft FReft
• type RefType = RRType FReft
• type PrType = RRType Predicate
• type SpecType = RRType RReft
• data PVar t = PV {
  • pname :: !Symbol
  • ptype :: !t
  • pargs :: ![(t, Symbol, Expr)]
  }
• newtype Predicate = Pr [UsedPVar]
• data UReft r = U {
  • ur_reft :: !r
  • ur_pred :: !Predicate
  }
• data DataDecl = D {
  • tycName :: String
  • tycTyVars :: [String]
  • tycPVars :: [PVar BSort]
  • tycDCons :: [(String, [(String, BareType)])]
  }
• uTop :: r -> UReft r
• uReft :: (Symbol, [Refa]) -> UReft Reft
• uRType :: RType p c tv a -> RType p c tv (UReft a)
• uRType' :: RType p c tv (UReft a) -> RType p c tv a
• uRTypeGen :: Reftable b => RType p c tv a -> RType p c tv b
• uPVar :: PVar t -> UsedPVar
• pdAnd :: [Predicate] -> Predicate
• pdVar :: PVar t -> Predicate
• pdTrue :: Predicate
• pvars :: Predicate -> [UsedPVar]
• findPVar :: [PVar (RType p c tv ())] -> UsedPVar -> PVar (RType p c tv ())
• ppr_rtype :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> 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 -> c1
• foldReft :: Reftable r => (r -> c1 -> c1) -> c1 -> RType p c tv r -> c1
• mapReft :: (r1 -> r2) -> RType p c tv r1 -> RType p c tv r2
• mapReftM :: Monad m => (r1 -> m r2) -> RType p c tv r1 -> m (RType p c tv r2)
• mapBot :: (RType p c tv s -> RType p c tv s) -> RType p c tv s -> RType p c tv s
• mapBind :: (Symbol -> Symbol) -> RType p c tv r -> RType p c tv r
• freeTyVars :: RefTypable t t1 a t2 => RType t t1 a t2 -> [a]
• tyClasses :: RefTypable t3 t t1 t2 => RType t3 t t1 t2 -> [(t3, [RType t3 t t1 t2])]
• ofType :: Reftable r => Type -> RRType r
• ofPredTree :: Reftable r => PredTree -> RType Class RTyCon RTyVar r
• toType :: Reftable r => RRType r -> Type
• rTyVar :: TyVar -> RTyVar
• rVar :: Reftable r => TyVar -> RType p c RTyVar r
• rApp :: TyCon -> [RType p RTyCon tv r] -> [Ref r (RType p RTyCon tv r)] -> r -> RType p RTyCon tv r
• rFun :: Reftable r => Symbol -> RType p c tv r -> RType p c tv r -> RType p c tv r
• expandRApp :: Reftable r => HashMap TyCon RTyCon -> RType Class RTyCon RTyVar r -> RType Class RTyCon RTyVar r
• typeUniqueSymbol :: Type -> Symbol
• strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv r
• mkArrow :: Reftable r => [a] -> [PVar (RType p c a ())] -> [(Symbol, RType p c a r)] -> RType p c a r -> RType p c a r
• mkUnivs :: [a] -> [PVar (RType p c a ())] -> RType p c a r -> RType p c a r
• bkUniv :: RType t t1 a t2 -> ([a], [PVar (RType t t1 a ())], RType t t1 a t2)
• bkArrow :: RType t t1 t2 t3 -> ([Symbol], [RType t t1 t2 t3], RType t t1 t2 t3)
• generalize :: RefTypable p c a r => RType p c a r -> RType p c a r
• normalizePds :: RefTypable p c tv r => RType p c tv r -> RType p c tv r
• subts :: SubsTy tv ty c => [(tv, ty)] -> c -> c
• subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
• subvUReft :: (UsedPVar -> UsedPVar) -> UReft FReft -> UReft FReft
• 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 s
• 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 s
• 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 s
• 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 s
• stripRTypeBase :: RType t t1 t2 a -> Maybe a
• rTypeReft :: Reftable r => RType p c tv r -> Reft
• rTypeSortedReft :: Reftable r => TCEmb TyCon -> RRType r -> SortedReft
• rTypeSort :: Reftable r => TCEmb TyCon -> RRType r -> Sort
• rTypeValueVar :: Reftable r => RType p c tv r -> Symbol
• ofRSort :: Reftable r => RType p c tv () -> RType p c tv r
• toRSort :: RType p c tv r -> RType p c tv ()
• varSymbol :: Var -> Symbol
• dataConSymbol :: DataCon -> Symbol
• dataConMsReft :: Reftable r => RType p c tv r -> [Symbol] -> FReft
• dataConReft :: DataCon -> [Symbol] -> FReft
• literalFRefType :: TCEmb TyCon -> Literal -> RType p RTyCon RTyVar FReft
• literalFReft :: TCEmb TyCon -> Literal -> FReft
• literalConst :: TCEmb TyCon -> Literal -> (Sort, Expr)
• fromRMono :: [Char] -> Ref t t1 -> t
• fromRPoly :: Ref t t1 -> t1
• idRMono :: Ref b t -> Ref b m
• isTrivial :: Reftable r => RType p c tv r -> Bool

Documentation

Functions for lifting Reft-values to Spec-values

Functions for manipulating Predicates

Traversing RType