@@ -5,6 +5,27 @@ module Idris.ASTUtils where
55--
66-- We don't include an explicit export list
77-- because everything here is meant to be exported.
8+--
9+-- Short synopsis:
10+-- ---------------
11+--
12+-- f :: Idris ()
13+-- f = do
14+-- -- these two steps:
15+-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
16+-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
17+--
18+-- -- are equivalent to:
19+-- fmodifyState (opt_detaggable . ist_optimisation typeName) not
20+--
21+-- -- of course, the long accessor can be put in a variable;
22+-- -- everything is first-class
23+-- let detag n = opt_detaggable . ist_optimisation n
24+-- fputState (detag n1) True
25+-- fputState (detag n2) False
26+--
27+-- -- Note that all these operations handle missing items consistently
28+-- -- and transparently, as prescribed by the typeclass InitialValue.
829
930import Control.Category
1031import Control.Applicative
@@ -54,6 +75,9 @@ ctxt_lookupExact n = Field
5475-----------------------------------
5576-- Individual records and fields --
5677-----------------------------------
78+--
79+-- These could probably be generated; let's use lazy addition for now.
80+--
5781
5882
5983-- OptInfo