[Agda] Refactoring typechecking monads

[Favonia]

Dear Agda hackers,

One of my proposals at the last AIX was to refactor the typechecking monad
(TCM).  The goal is to clean up the current codebase so that a good Haskell
API is immediately available.  I'd like to break the typechecking monad
into several monads, including but not limited to

1. scope checking
2. type checking

I'm still working on this, and I plan to refactor the program gradually.
Some smaller patches have been merged into the codebase.  I have one
architectural question and one technical question though:

[arch]: If there should be a "master" monad invoking the type checking and
scope checking, what should it be?

[tech]: TCM is using IORef to hold the states.  Is IORef significantly
faster than StateT or other equivalent?  If references are really superior,
how about the ST monad?

As I'm refactoring the code gradually, my next target is interaction
points.  I'd like to create a separate monad for scope checking and move
interaction points from TCState to other places.

Thanks,
Favonia
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140620/b34c2214/attachment.html