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