@@ -5,6 +5,27 @@ module Idris.ASTUtils where
6-- We don't include an explicit export list
6-- We don't include an explicit export list
7-- because everything here is meant to be exported.
7-- because everything here is meant to be exported.
14+-- -- these two steps:
15+-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
16+-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
18+-- -- are equivalent to:
19+-- fmodifyState (opt_detaggable . ist_optimisation typeName) not
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
27+-- -- Note that all these operations handle missing items consistently
28+-- -- and transparently, as prescribed by the typeclass InitialValue.
9import Control.Category
30import Control.Category
10import Control.Applicative
31import Control.Applicative
@@ -54,6 +75,9 @@ ctxt_lookupExact n = Field
54-----------------------------------
75-----------------------------------
55-- Individual records and fields --
76-- Individual records and fields --
56-----------------------------------
77-----------------------------------
79+-- These could probably be generated; let's use lazy addition for now.