FoobarE.idr

module FoobarE

import Effects
import Effect.State
import Effect.StdIO

namespace Lib
  MyLib : Type -> Type
  MyLib rTy = Eff rTy ['libstate ::: STATE (List Nat), STDIO]

  register : Nat -> MyLib ()
  register x = 'libstate :- update (x::)

  count : MyLib Nat
  count = pure (length !('libstate :- get))

namespace User
  User : Type -> Type
  User rTy = Eff rTy [ 'libstate ::: STATE (List Nat)
                     , 'mystate ::: STATE (List Nat)
                     , STDIO]

  wipe : User ()
  wipe = 'libstate :- put Nil

myProg : User ()
myProg = do
  register 1
  register 2
  printLn !count
  wipe
  register 3
  register 4
  printLn !count


namespace Main
  main : IO ()
  main = run myProg