@@ -25,7 +25,11 @@ module Idris.ASTUtils where
2525-- fputState (detag n2) False
2626--
2727-- -- Note that all these operations handle missing items consistently
28−-- -- and transparently, as prescribed by the typeclass InitialValue.
28+-- -- and transparently, as prescribed by the default values included
29+-- -- in the definitions of the ist_* functions.
30+-- --
31+-- -- Especially, it's no longer necessary to have initial values of
32+-- -- data structures copied (possibly inconsistently) all over the compiler.
2933
3034import Control.Category
3135import Control.Applicative
@@ -57,20 +61,22 @@ fputState field x = fmodifyState field (const x)
5761fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
5862fmodifyState field f = modify $ fmodify field f
5963
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
64+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
65+--
66+-- Reading a non-existing value yields Nothing,
67+-- writing Nothing deletes the value (if it existed).
68+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
69+ctxt_lookup n = Field
70+ { fget = lookupCtxtExact n
71+ , fset = \newVal -> case newVal of
72+ Just x -> addDef n x
73+ Nothing -> deleteDefExact n
7274 }
7375
76+-- Maybe-lens with a default value.
77+maybe_default :: a -> Field (Maybe a) a
78+maybe_default dflt = Field (fromMaybe dflt) (const . Just)
79+
7480
7581-----------------------------------
7682-- Individual records and fields --
@@ -83,12 +89,14 @@ ctxt_lookupExact n = Field
8389-- OptInfo
8490----------
8591
86−instance InitialValue OptInfo where
87− initialValue = Optimise [] False
88−
8992-- the optimisation record for the given (exact) name
9093ist_optimisation :: Name -> Field IState OptInfo
91−ist_optimisation n = ctxt_lookupExact n
94+ist_optimisation n =
95+ maybe_default Optimise
96+ { inaccessible = []
97+ , detaggable = False
98+ }
99+ . ctxt_lookup n
92100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
93101
94102-- two fields of the optimisation record
@@ -102,12 +110,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
102110-- CGInfo
103111---------
104112
105−instance InitialValue CGInfo where
106− initialValue = CGInfo [] [] [] [] []
107−
108113-- callgraph record for the given (exact) name
109114ist_callgraph :: Name -> Field IState CGInfo
110−ist_callgraph n = ctxt_lookupExact n
115+ist_callgraph n =
116+ maybe_default CGInfo
117+ { argsdef = [], calls = [], scg = []
118+ , argsused = [], usedpos = []
119+ }
120+ . ctxt_lookup n
111121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
112122
113123-- some fields of the CGInfo record