{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Agda.TypeChecking.Conversion.Pure where

import Control.Monad.Fail (MonadFail)
import Control.Monad.State

import Data.String

import Agda.Syntax.Common
import Agda.Syntax.Internal

import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Warnings

import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Null

import Agda.Utils.Impossible

data FreshThings = FreshThings
  { FreshThings -> Int
freshInt       :: Int
  , FreshThings -> ProblemId
freshProblemId :: ProblemId
  , FreshThings -> NameId
freshNameId    :: NameId
  }

newtype PureConversionT m a = PureConversionT
  { PureConversionT m a -> ExceptT TCErr (StateT FreshThings m) a
unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a }
  deriving (a -> PureConversionT m b -> PureConversionT m a
(a -> b) -> PureConversionT m a -> PureConversionT m b
(forall a b.
 (a -> b) -> PureConversionT m a -> PureConversionT m b)
-> (forall a b. a -> PureConversionT m b -> PureConversionT m a)
-> Functor (PureConversionT m)
forall a b. a -> PureConversionT m b -> PureConversionT m a
forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
forall (m :: * -> *) a b.
Functor m =>
a -> PureConversionT m b -> PureConversionT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PureConversionT m a -> PureConversionT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> PureConversionT m b -> PureConversionT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PureConversionT m b -> PureConversionT m a
fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PureConversionT m a -> PureConversionT m b
Functor, Functor (PureConversionT m)
a -> PureConversionT m a
Functor (PureConversionT m)
-> (forall a. a -> PureConversionT m a)
-> (forall a b.
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b)
-> (forall a b c.
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c)
-> (forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
-> (forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a)
-> Applicative (PureConversionT m)
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
forall a. a -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall a b.
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
forall a b c.
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
forall (m :: * -> *). Monad m => Functor (PureConversionT m)
forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: PureConversionT m a -> PureConversionT m b -> PureConversionT m a
$c<* :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
*> :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b
$c*> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
liftA2 :: (a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
<*> :: PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
pure :: a -> PureConversionT m a
$cpure :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
$cp1Applicative :: forall (m :: * -> *). Monad m => Functor (PureConversionT m)
Applicative, Applicative (PureConversionT m)
a -> PureConversionT m a
Applicative (PureConversionT m)
-> (forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b)
-> (forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
-> (forall a. a -> PureConversionT m a)
-> Monad (PureConversionT m)
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall a. a -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall a b.
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
forall (m :: * -> *). Monad m => Applicative (PureConversionT m)
forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> PureConversionT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
>> :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
>>= :: PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (PureConversionT m)
Monad, MonadError TCErr, MonadState FreshThings)

pureEqualTerm
  :: (MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m)
  => Type -> Term -> Term -> m Bool
pureEqualTerm :: Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v = Lens' Bool TCEnv -> (Bool -> Bool) -> m Bool -> m Bool
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eCompareBlocked (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$
  Either TCErr () -> Bool
forall a b. Either a b -> Bool
isRight (Either TCErr () -> Bool) -> m (Either TCErr ()) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Either TCErr ())
forall (m :: * -> *) a.
(ReadTCState m, MonadDebug m, HasOptions m, MonadTCEnv m,
 Show a) =>
PureConversionT m a -> m (Either TCErr a)
runPureConversion (Type -> Term -> Term -> PureConversionT m ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v)

pureCompareAs
  :: (MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m)
  => Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs Comparison
cmp CompareAs
a Term
u Term
v = Lens' Bool TCEnv -> (Bool -> Bool) -> m Bool -> m Bool
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eCompareBlocked (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$
  Either TCErr () -> Bool
forall a b. Either a b -> Bool
isRight (Either TCErr () -> Bool) -> m (Either TCErr ()) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Either TCErr ())
forall (m :: * -> *) a.
(ReadTCState m, MonadDebug m, HasOptions m, MonadTCEnv m,
 Show a) =>
PureConversionT m a -> m (Either TCErr a)
runPureConversion (Comparison -> CompareAs -> Term -> Term -> PureConversionT m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
a Term
u Term
v)

runPureConversion
  :: (ReadTCState m, MonadDebug m, HasOptions m, MonadTCEnv m, Show a)
  => PureConversionT m a -> m (Either TCErr a)
runPureConversion :: PureConversionT m a -> m (Either TCErr a)
runPureConversion (PureConversionT ExceptT TCErr (StateT FreshThings m) a
m) = do
  Int
i <- Lens' Int TCState -> m Int
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Int TCState
stFreshInt
  ProblemId
pid <- Lens' ProblemId TCState -> m ProblemId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ProblemId TCState
stFreshProblemId
  NameId
nid <- Lens' NameId TCState -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' NameId TCState
stFreshNameId
  let frsh :: FreshThings
frsh = Int -> ProblemId -> NameId -> FreshThings
FreshThings Int
i ProblemId
pid NameId
nid
  Either TCErr a
result <- (Either TCErr a, FreshThings) -> Either TCErr a
forall a b. (a, b) -> a
fst ((Either TCErr a, FreshThings) -> Either TCErr a)
-> m (Either TCErr a, FreshThings) -> m (Either TCErr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FreshThings m (Either TCErr a)
-> FreshThings -> m (Either TCErr a, FreshThings)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ExceptT TCErr (StateT FreshThings m) a
-> StateT FreshThings m (Either TCErr a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT TCErr (StateT FreshThings m) a
m) FreshThings
frsh
  VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.conv.pure" Int
40 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"runPureConversion result: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Either TCErr a -> VerboseKey
forall a. Show a => a -> VerboseKey
show Either TCErr a
result
  Either TCErr a -> m (Either TCErr a)
forall (m :: * -> *) a. Monad m => a -> m a
return Either TCErr a
result

deriving instance MonadFail       m => MonadFail       (PureConversionT m)
deriving instance HasBuiltins     m => HasBuiltins     (PureConversionT m)
deriving instance HasConstInfo    m => HasConstInfo    (PureConversionT m)
deriving instance HasOptions      m => HasOptions      (PureConversionT m)
deriving instance MonadTCEnv      m => MonadTCEnv      (PureConversionT m)
deriving instance ReadTCState     m => ReadTCState     (PureConversionT m)
deriving instance MonadReduce     m => MonadReduce     (PureConversionT m)
deriving instance MonadAddContext m => MonadAddContext (PureConversionT m)
deriving instance MonadDebug      m => MonadDebug      (PureConversionT m)

instance (Monad m, Semigroup a) => Semigroup (PureConversionT m a) where
  PureConversionT m a
d1 <> :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a
<> PureConversionT m a
d2 = a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) (a -> a -> a) -> PureConversionT m a -> PureConversionT m (a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m a
d1 PureConversionT m (a -> a)
-> PureConversionT m a -> PureConversionT m a
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PureConversionT m a
d2

instance (IsString a, Monad m) => IsString (PureConversionT m a) where
  fromString :: VerboseKey -> PureConversionT m a
fromString VerboseKey
s = a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> a
forall a. IsString a => VerboseKey -> a
fromString VerboseKey
s)

instance Monad m => Null (PureConversionT m Doc) where
  empty :: PureConversionT m Doc
empty = Doc -> PureConversionT m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Null a => a
empty
  null :: PureConversionT m Doc -> Bool
null = PureConversionT m Doc -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance (MonadTCEnv m, ReadTCState m, HasOptions m, MonadDebug m)
  => MonadConstraint (PureConversionT m) where
  addConstraint :: Constraint -> PureConversionT m ()
addConstraint Constraint
c = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  addAwakeConstraint :: Constraint -> PureConversionT m ()
addAwakeConstraint Constraint
c = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  catchPatternErr :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a
catchPatternErr PureConversionT m a
handle PureConversionT m a
m = PureConversionT m a
m PureConversionT m a
-> (TCErr -> PureConversionT m a) -> PureConversionT m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    PatternErr{} -> PureConversionT m a
handle
    TCErr
err          -> TCErr -> PureConversionT m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  solveConstraint :: Constraint -> PureConversionT m ()
solveConstraint Constraint
c = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
_ Bool
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  wakeConstraints :: (ProblemConstraint -> PureConversionT m Bool)
-> PureConversionT m ()
wakeConstraints ProblemConstraint -> PureConversionT m Bool
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  stealConstraints :: ProblemId -> PureConversionT m ()
stealConstraints ProblemId
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifyAwakeConstraints Constraints -> Constraints
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifySleepingConstraints Constraints -> Constraints
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation

instance (MonadTCEnv m, MonadReduce m, MonadAddContext m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m)
  => MonadMetaSolver (PureConversionT m) where
  newMeta' :: MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> PureConversionT m MetaId
newMeta' MetaInstantiation
_ Frozen
_ MetaInfo
_ MetaPriority
_ Permutation
_ Judgement a
_ = PureConversionT m MetaId
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> PureConversionT m ()
assignV CompareDirection
_ MetaId
_ Args
_ Term
_ CompareAs
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  assignTerm' :: MetaId -> [Arg VerboseKey] -> Term -> PureConversionT m ()
assignTerm' MetaId
_ [Arg VerboseKey]
_ Term
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()
etaExpandMeta [MetaKind]
_ MetaId
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
updateMetaVar MetaId
_ MetaVariable -> MetaVariable
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  speculateMetas :: PureConversionT m ()
-> PureConversionT m KeepMetas -> PureConversionT m ()
speculateMetas PureConversionT m ()
fallback PureConversionT m KeepMetas
m = PureConversionT m KeepMetas
m PureConversionT m KeepMetas
-> (KeepMetas -> PureConversionT m ()) -> PureConversionT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    KeepMetas
KeepMetas     -> () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    KeepMetas
RollBackMetas -> PureConversionT m ()
fallback

instance (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints (PureConversionT m) where
  freshInteractionId :: PureConversionT m InteractionId
freshInteractionId = PureConversionT m InteractionId
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
_ = PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation

-- This is a bogus instance that promptly forgets all concrete names,
-- but we don't really care
instance ReadTCState m => MonadStConcreteNames (PureConversionT m) where
  runStConcreteNames :: StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a
runStConcreteNames StateT ConcreteNames (PureConversionT m) a
m = do
    ConcreteNames
concNames <- Lens' ConcreteNames TCState -> PureConversionT m ConcreteNames
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ConcreteNames TCState
stConcreteNames
    (a, ConcreteNames) -> a
forall a b. (a, b) -> a
fst ((a, ConcreteNames) -> a)
-> PureConversionT m (a, ConcreteNames) -> PureConversionT m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ConcreteNames (PureConversionT m) a
-> ConcreteNames -> PureConversionT m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (PureConversionT m) a
m ConcreteNames
concNames

instance (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m)
  => MonadWarning (PureConversionT m) where
  addWarning :: TCWarning -> PureConversionT m ()
addWarning TCWarning
w = case Warning -> WhichWarnings
classifyWarning (TCWarning -> Warning
tcWarning TCWarning
w) of
    WhichWarnings
ErrorWarnings -> PureConversionT m ()
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
    WhichWarnings
AllWarnings   -> () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance ReadTCState m => MonadStatistics (PureConversionT m) where
  modifyCounter :: VerboseKey -> (Integer -> Integer) -> PureConversionT m ()
modifyCounter VerboseKey
_ Integer -> Integer
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance Monad m => MonadFresh ProblemId (PureConversionT m) where
  fresh :: PureConversionT m ProblemId
fresh = do
    ProblemId
i <- (FreshThings -> ProblemId) -> PureConversionT m ProblemId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> ProblemId
freshProblemId
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshProblemId :: ProblemId
freshProblemId = ProblemId
i ProblemId -> ProblemId -> ProblemId
forall a. Num a => a -> a -> a
+ ProblemId
1 }
    ProblemId -> PureConversionT m ProblemId
forall (m :: * -> *) a. Monad m => a -> m a
return ProblemId
i

instance Monad m => MonadFresh NameId (PureConversionT m) where
  fresh :: PureConversionT m NameId
fresh = do
    NameId
i <- (FreshThings -> NameId) -> PureConversionT m NameId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> NameId
freshNameId
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshNameId :: NameId
freshNameId = NameId -> NameId
forall a. Enum a => a -> a
succ NameId
i }
    NameId -> PureConversionT m NameId
forall (m :: * -> *) a. Monad m => a -> m a
return NameId
i

instance Monad m => MonadFresh Int (PureConversionT m) where
  fresh :: PureConversionT m Int
fresh = do
    Int
i <- (FreshThings -> Int) -> PureConversionT m Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> Int
freshInt
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshInt :: Int
freshInt = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
    Int -> PureConversionT m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i