{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE TypeFamilies #-}
module Gyehoek.GenSym where

import Numeric.Natural
import Effectful.State.Dynamic
import Effectful.Dispatch.Dynamic
import Effectful
import Language.QBE as QBE
import Data.String (IsString(fromString))
import Data.Text (Text)
import qualified Data.Text.Short as ST


class Gen a where
  gen :: Natural -> a
  gen' :: Text -> Natural -> a

data GenSym :: Effect where
  GenSym :: Gen a => GenSym m a
  GenSym' :: Gen a => Text -> GenSym m a

type instance DispatchOf GenSym = Dynamic

gensym :: forall a es. (Gen a, GenSym :> es) => Eff es a
gensym = send GenSym

gensym' :: forall a es. (Gen a, GenSym :> es) => Text -> Eff es a
gensym' = send . GenSym'

runGenSym :: Eff (GenSym : es) a -> Eff es a
runGenSym = reinterpret (evalStateLocal (0 :: Natural)) \cases
  _ GenSym -> state \n -> (gen n, succ n)
  _ (GenSym' s) -> state \n -> (gen' s n, succ n)

instance Gen (QBE.Ident s) where
  gen = Ident . fromString . ('.':) . show
  gen' s = Ident . (ST.fromText s <>) . fromString . show

instance Gen Text where
  gen = fromString . ('x':) . show
  gen' s = (s <>) . fromString . show