Language.Haskell.Liquid.Types.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 RReft

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m RReft

true :: RReft -> m RReft

refresh :: RReft -> m RReft

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

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m Reft

true :: Reft -> m Reft

refresh :: Reft -> m Reft

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

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m Expr

true :: Expr -> m Expr

refresh :: Expr -> m Expr

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

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m Symbol

true :: Symbol -> m Symbol

refresh :: Symbol -> m Symbol

Freshable CG Integer

This is all hardwiring stuff to CG ----------------------------------------

Defined in Language.Haskell.Liquid.Constraint.Fresh

Methods

fresh :: CG Integer

true :: Integer -> CG Integer

refresh :: Integer -> CG Integer

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

Defined in Language.Haskell.Liquid.Types.Fresh

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]

Defined in Language.Haskell.Liquid.Types.Fresh

Methods

fresh :: m [Expr]

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

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

refreshTy :: FreshM m => SpecType -> m SpecType

refreshVV :: FreshM m => SpecType -> m SpecType

refreshArgs :: FreshM m => SpecType -> m SpecType

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

refreshArgsSub :: FreshM m => SpecType -> m (SpecType, Subst)