@@ -57,20 +57,22 @@ fputState field x = fmodifyState field (const x)
5757fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
5858fmodifyState field f = modify $ fmodify field f
5959
60−-- Until now, we'd have just ad-hoc empty lists and Falses thrown around
61−-- whenever a new instance of a record was to be created.
62−--
63−-- This class formalises the notion of an initial value for a record.
64−class InitialValue a where
65− initialValue :: a
66−
67−-- Exact-name context lookup; uses the initial value if needed.
68−ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
69−ctxt_lookupExact n = Field
70− { fget = fromMaybe initialValue . lookupCtxtExact n
71− , fset = addDef n
60+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
61+--
62+-- Reading a non-existing value yields Nothing,
63+-- writing Nothing deletes the value (if it existed).
64+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
65+ctxt_lookup n = Field
66+ { fget = lookupCtxtExact n
67+ , fset = \newVal -> case newVal of
68+ Just x -> addDef n x
69+ Nothing -> deleteDefExact n
7270 }
7371
72+-- Maybe-lens with a default value.
73+maybe_default :: a -> Field (Maybe a) a
74+maybe_default dflt = Field (fromMaybe dflt) (const . Just)
75+
7476
7577-----------------------------------
7678-- Individual records and fields --
@@ -83,12 +85,14 @@ ctxt_lookupExact n = Field
8385-- OptInfo
8486----------
8587
86−instance InitialValue OptInfo where
87− initialValue = Optimise [] False
88−
8988-- the optimisation record for the given (exact) name
9089ist_optimisation :: Name -> Field IState OptInfo
91−ist_optimisation n = ctxt_lookupExact n
90+ist_optimisation n =
91+ maybe_default Optimise
92+ { inaccessible = []
93+ , detaggable = False
94+ }
95+ . ctxt_lookup n
9296 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
9397
9498-- two fields of the optimisation record
@@ -102,12 +106,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
102106-- CGInfo
103107---------
104108
105−instance InitialValue CGInfo where
106− initialValue = CGInfo [] [] [] [] []
107−
108109-- callgraph record for the given (exact) name
109110ist_callgraph :: Name -> Field IState CGInfo
110−ist_callgraph n = ctxt_lookupExact n
111+ist_callgraph n =
112+ maybe_default CGInfo
113+ { argsdef = [], calls = [], scg = []
114+ , argsused = [], usedpos = []
115+ }
116+ . ctxt_lookup n
111117 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
112118
113119-- some fields of the CGInfo record