Language.Haskell.Liquid.Constraint.Fresh

Documentation

class (Applicative m, Monad m) => Freshable m a where

Minimal complete definition

fresh

Methods

fresh :: m a

true :: a -> m a

refresh :: a -> m a

Instances

Freshable m Integer => Freshable m Strata

Methods

fresh :: m Strata

true :: Strata -> m Strata

refresh :: Strata -> m Strata

Freshable m Integer => Freshable m RReft

Methods

fresh :: m RReft

true :: RReft -> m RReft

refresh :: RReft -> m RReft

(Freshable m Integer, Monad m, Applicative m) => Freshable m Reft

Methods

fresh :: m Reft

true :: Reft -> m Reft

refresh :: Reft -> m Reft

(Freshable m Integer, Monad m, Applicative m) => Freshable m Expr

Methods

fresh :: m Expr

true :: Expr -> m Expr

refresh :: Expr -> m Expr

(Freshable m Integer, Monad m, Applicative m) => Freshable m Symbol

Methods

fresh :: m Symbol

true :: Symbol -> m Symbol

refresh :: Symbol -> m Symbol

Freshable CG Integer

Methods

fresh :: CG Integer

true :: Integer -> CG Integer

refresh :: Integer -> CG Integer

(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r)

Methods

fresh :: m (RRType r)

true :: RRType r -> m (RRType r)

refresh :: RRType r -> m (RRType r)

(Freshable m Integer, Monad m, Applicative m) => Freshable m [Expr]

Methods

fresh :: m [Expr]

true :: [Expr] -> m [Expr]

refresh :: [Expr] -> m [Expr]

refreshTy :: SpecType -> CG SpecType

refreshVV :: Freshable m Integer => SpecType -> m SpecType

refreshArgs :: SpecType -> CG SpecType

refreshArgsTop :: (Var, SpecType) -> CG SpecType

refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])

freshTy_type :: KVKind -> CoreExpr -> Type -> CG SpecType

Generation: Freshness -----------------------------------------------------

Right now, we generate NO new pvars. Rather than clutter code with uRType calls, put it in one place where the above invariant is obviously enforced. Constraint generation should ONLY use freshTy_type and freshTy_expr

freshTy_expr :: KVKind -> CoreExpr -> Type -> CG SpecType

trueTy :: Type -> CG SpecType

addKuts :: PPrint a => a -> SpecType -> CG ()