Safe Haskell	None
Language	Haskell98

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

Instances details

Freshable m Integer => Freshable m RReft #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 ----------------------------------------
Instance details 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) #
Instance details 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] #
Instance details 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) #