idris-lang/Idris-dev — pull request #1065 by ziman (2014-04-14 16:48:55+00:00)
Title: Lens-style IState updates

This patch adds lens-style updates to `IState`, fixing a related bug, which caused missing erasure warnings by overwriting an already initialised field.

The core of the lens mechanism is implemented in ~30 lines of Haskell, which is hopefully a good reason to avoid:
* a direct dependency on `lens`, in case we want to move away from it in the future;
* an additional dependency on `fclabels`, which is similar to this approach.
In return, we get convenient field access and updates, together with systematically added default values instead of ad-hoc `CGInfo [] [] True [] False`-style initialisations sprinkled all over the code.

The patch also includes changes to use the new field access style in several places of the codebase.

A short example:
```Haskell
f :: Idris ()
f = do
-- these two steps:
detaggable <- fgetState (opt_detaggable . ist_optimisation n)
fputState (opt_detaggable . ist_optimisation n) (not detaggable)

-- are equivalent to:
fmodifyState (opt_detaggable . ist_optimisation n) not

-- of course, the long accessor can be aliased; everything is first-class
let detag n = opt_detaggable . ist_optimisation n
fputState (detag n1) True
fputState (detag n2) False

-- Note that all these operations handle missing items consistently
-- and transparently, as prescribed by the typeclass InitialValue.
```