@@ -57,20 +57,22 @@ fputState field x = fmodifyState field (const x)
57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
58fmodifyState field f = modify $ fmodify field f
58fmodifyState field f = modify $ fmodify field f
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.
63−-- This class formalises the notion of an initial value for a record.
64−class InitialValue a where
67−-- Exact-name context lookup; uses the initial value if needed.
60+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
62+-- Reading a non-existing value yields Nothing,
63+-- writing Nothing deletes the value (if it existed).
68−ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
64+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
69−ctxt_lookupExact n = Field
65+ctxt_lookup n = Field
70− { fget = fromMaybe initialValue . lookupCtxtExact n
66+ { fget = lookupCtxtExact n
67+ , fset = \newVal -> case newVal of
71− , fset = addDef n
68+ Just x -> addDef n x
69+ Nothing -> deleteDefExact n
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-----------------------------------
77-----------------------------------
76-- Individual records and fields --
78-- Individual records and fields --
@@ -83,12 +85,14 @@ ctxt_lookupExact n = Field
86−instance InitialValue OptInfo where
87− initialValue = Optimise [] False
89-- the optimisation record for the given (exact) name
88-- the optimisation record for the given (exact) name
90ist_optimisation :: Name -> Field IState OptInfo
89ist_optimisation :: Name -> Field IState OptInfo
91−ist_optimisation n = ctxt_lookupExact n
90+ist_optimisation n =
91+ maybe_default Optimise
92 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
96 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
94-- two fields of the optimisation record
98-- two fields of the optimisation record
@@ -102,12 +106,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
105−instance InitialValue CGInfo where
106− initialValue = CGInfo [] [] [] [] []
108-- callgraph record for the given (exact) name
109-- callgraph record for the given (exact) name
109ist_callgraph :: Name -> Field IState CGInfo
110ist_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 = []
111 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
117 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
113-- some fields of the CGInfo record
119-- some fields of the CGInfo record