git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/ASTUtils.hs
159 lines 5.2 kB history raw
1module Idris.ASTUtils(Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState,
2 fputState, idris_fixities, ist_callgraph, ist_optimisation,
3 known_classes, known_terms, opt_detaggable, opt_inaccessible,
4 opts_idrisCmdline, repl_definitions) where
6-- This implements just a few basic lens-like concepts to ease state updates.
7-- Similar to fclabels in approach, just without the extra dependency.
8--
9-- We don't include an explicit export list
10-- because everything here is meant to be exported.
11--
12-- Short synopsis:
13-- ---------------
14--
15-- f :: Idris ()
16-- f = do
17-- -- these two steps:
18-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
19-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
20--
21-- -- are equivalent to:
22-- fmodifyState (opt_detaggable . ist_optimisation typeName) not
23--
24-- -- of course, the long accessor can be put in a variable;
25-- -- everything is first-class
26-- let detag n = opt_detaggable . ist_optimisation n
27-- fputState (detag n1) True
28-- fputState (detag n2) False
29--
30-- -- Note that all these operations handle missing items consistently
31-- -- and transparently, as prescribed by the default values included
32-- -- in the definitions of the ist_* functions.
33-- --
34-- -- Especially, it's no longer necessary to have initial values of
35-- -- data structures copied (possibly inconsistently) all over the compiler.
37import Control.Category
38import Control.Applicative
39import Control.Monad.State.Class
40import Data.Maybe
41import Prelude hiding (id, (.))
43import Idris.Core.TT
44import Idris.Core.Evaluate
45import Idris.AbsSyntaxTree
47data Field rec fld = Field
48 { fget :: rec -> fld
49 , fset :: fld -> rec -> rec
50 }
52fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
53fmodify field f x = fset field (f $ fget field x) x
55instance Category Field where
56 id = Field id const
57 Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
59fgetState :: MonadState s m => Field s a -> m a
60fgetState field = gets $ fget field
62fputState :: MonadState s m => Field s a -> a -> m ()
63fputState field x = fmodifyState field (const x)
65fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
66fmodifyState field f = modify $ fmodify field f
68-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
69--
70-- Reading a non-existing value yields Nothing,
71-- writing Nothing deletes the value (if it existed).
72ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
73ctxt_lookup n = Field
74 { fget = lookupCtxtExact n
75 , fset = \newVal -> case newVal of
76 Just x -> addDef n x
77 Nothing -> deleteDefExact n
78 }
80-- Maybe-lens with a default value.
81maybe_default :: a -> Field (Maybe a) a
82maybe_default dflt = Field (fromMaybe dflt) (const . Just)
85-----------------------------------
86-- Individual records and fields --
87-----------------------------------
88--
89-- These could probably be generated; let's use lazy addition for now.
90--
93-- OptInfo
94----------
96-- the optimisation record for the given (exact) name
97ist_optimisation :: Name -> Field IState OptInfo
98ist_optimisation n =
99 maybe_default Optimise
100 { inaccessible = []
101 , detaggable = False
102 }
103 . ctxt_lookup n
104 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
106-- two fields of the optimisation record
107opt_inaccessible :: Field OptInfo [(Int, Name)]
108opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
110opt_detaggable :: Field OptInfo Bool
111opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
114-- CGInfo
115---------
117-- callgraph record for the given (exact) name
118ist_callgraph :: Name -> Field IState CGInfo
119ist_callgraph n =
120 maybe_default CGInfo
121 { argsdef = [], calls = [], scg = []
122 , argsused = [], usedpos = []
123 }
124 . ctxt_lookup n
125 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
127-- some fields of the CGInfo record
128cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
129cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })
132-- Commandline flags
133--------------------
135opts_idrisCmdline :: Field IState [Opt]
136opts_idrisCmdline =
137 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })
138 . Field idris_options (\v ist -> ist{ idris_options = v })
140-- TT Context
141-------------
142-- This has a terrible name, but I'm not sure of a better one that isn't
143-- confusingly close to tt_ctxt
144known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))
145known_terms = Field (definitions . tt_ctxt)
146 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
148known_classes :: Field IState (Ctxt ClassInfo)
149known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})
152-- Names defined at the repl
153----------------------------
154repl_definitions :: Field IState [Name]
155repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})
157-- Fixity declarations in an IState
158idris_fixities :: Field IState [FixDecl]
159idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})