{-# LANGUAGE CPP
           , DataKinds
           , FlexibleInstances
           , FlexibleContexts
           , KindSignatures
           , OverloadedStrings
           , UndecidableInstances
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.Gensym where

#if __GLASGOW_HASKELL__ < 710
import           Data.Functor                    ((<$>))
#endif
import Control.Monad.State
import Data.Number.Nat
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing

class Monad m => Gensym m where
  freshVarId :: m Nat

instance (Monad m, MonadState Nat m) => Gensym m where
  freshVarId :: m Nat
freshVarId = do
    Nat
vid <- (Nat -> Nat) -> m Nat
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Nat -> Nat
forall a. Enum a => a -> a
succ
    Nat -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Nat
vid
    Nat -> m Nat
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
vid

freshVar
    :: (Functor m, Gensym m)
    => Variable (a :: Hakaru) -> m (Variable a)
freshVar :: Variable a -> m (Variable a)
freshVar Variable a
v = (Nat -> Variable a) -> m Nat -> m (Variable a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Nat
n -> Variable a
v{varID :: Nat
varID=Nat
n}) m Nat
forall (m :: * -> *). Gensym m => m Nat
freshVarId

varOfType
    :: (Functor m, Gensym m)
    => Sing (a :: Hakaru) -> m (Variable a)
varOfType :: Sing a -> m (Variable a)
varOfType Sing a
t = (Nat -> Variable a) -> m Nat -> m (Variable a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Nat
n  -> Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
"" Nat
n Sing a
t) m Nat
forall (m :: * -> *). Gensym m => m Nat
freshVarId

varForExpr
    :: (Functor m, Gensym m, ABT Term abt)
    => abt '[] a -> m (Variable a)
varForExpr :: abt '[] a -> m (Variable a)
varForExpr abt '[] a
v = (Nat -> Variable a) -> m Nat -> m (Variable a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Nat
n -> Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
"" Nat
n (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
v)) m Nat
forall (m :: * -> *). Gensym m => m Nat
freshVarId