diff options
| author | Pierre-Marie Pédrot | 2014-07-23 20:06:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-24 15:06:09 +0200 |
| commit | fb4187a6d475719bada0a7fe1b7902a36e06d658 (patch) | |
| tree | 4b628f26dc1911007baa997f5e371f0340cb8ec1 /kernel/cbytecodes.ml | |
| parent | a435938aa7d1c94c40ddb17627cfaa2fb9f45f0f (diff) | |
New implementation of the tactic monad.
The new implementation is made of two layers: a iolist, which is essentially
a stream without memoization, and above this a state monad. The previous
design of the extracted monad kept three distinct but similar monad
transformers: a stateT, a writerT and a readerT. We take advantage of this
similarity to pack those three transformers into only one state monad.
This makes the code cleaner and hopefully more efficient.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions
