tests

src/Gyehoek/GenSym.hs

@@ -0,0 +1,45 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE TypeFamilies #-}
+module Gyehoek.GenSym where
+
+import Numeric.Natural
+import Effectful.State.Dynamic
+import Effectful.Dispatch.Dynamic
+import Effectful
+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 Text where
+  gen = fromString . ('x':) . show
+  gen' s = (s <>) . fromString . show
+
+instance Gen Natural where
+  gen = id
+  gen' = const id
+
+instance Gen Int where
+  gen = fromIntegral
+  gen' _ = fromIntegral