@@ -25,7 +25,11 @@ module Idris.ASTUtils where
25-- fputState (detag n2) False
25-- fputState (detag n2) False
27-- -- Note that all these operations handle missing items consistently
27-- -- 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.
31+-- -- Especially, it's no longer necessary to have initial values of
32+-- -- data structures copied (possibly inconsistently) all over the compiler.
30import Control.Category
34import Control.Category
31import Control.Applicative
35import Control.Applicative
@@ -57,20 +61,22 @@ fputState field x = fmodifyState field (const x)
57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
61fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
58fmodifyState field f = modify $ fmodify field f
62fmodifyState 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.
64+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
66+-- Reading a non-existing value yields Nothing,
67+-- writing Nothing deletes the value (if it existed).
68−ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
68+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
69−ctxt_lookupExact n = Field
69+ctxt_lookup n = Field
70− { fget = fromMaybe initialValue . lookupCtxtExact n
70+ { fget = lookupCtxtExact n
71+ , fset = \newVal -> case newVal of
71− , fset = addDef n
72+ Just x -> addDef n x
73+ Nothing -> deleteDefExact n
76+-- Maybe-lens with a default value.
77+maybe_default :: a -> Field (Maybe a) a
78+maybe_default dflt = Field (fromMaybe dflt) (const . Just)
75-----------------------------------
81-----------------------------------
76-- Individual records and fields --
82-- Individual records and fields --
@@ -83,12 +89,14 @@ ctxt_lookupExact n = Field
86−instance InitialValue OptInfo where
87− initialValue = Optimise [] False
89-- the optimisation record for the given (exact) name
92-- the optimisation record for the given (exact) name
90ist_optimisation :: Name -> Field IState OptInfo
93ist_optimisation :: Name -> Field IState OptInfo
91−ist_optimisation n = ctxt_lookupExact n
94+ist_optimisation n =
95+ maybe_default Optimise
92 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
94-- two fields of the optimisation record
102-- two fields of the optimisation record
@@ -102,12 +110,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
113-- callgraph record for the given (exact) name
109ist_callgraph :: Name -> Field IState CGInfo
114ist_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 = []
111 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
113-- some fields of the CGInfo record
123-- some fields of the CGInfo record