{-# LANGUAGE MultiParamTypeClasses #-}

{-| A common interface for monads which allow some kind of fresh name
    generation.
-}
module Agda.Utils.Fresh where

import Control.Monad.State
import Control.Monad.Reader

class HasFresh i a where
    nextFresh :: a -> (i,a)

fresh :: (HasFresh i s, MonadState s m) => m i
fresh =
    do	(i,s) <- gets nextFresh
	put s
	return i

withFresh :: (HasFresh i e, MonadReader e m) => (i -> m a) -> m a
withFresh ret =
    do	(i,e) <- asks nextFresh
	local (const e) $ ret i