git.iko.soy/Idris-dev
on d16d418 help sign in
Idris-dev/src/Idris/ASTUtils.hs
134 lines 4.1 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.AbsSyntaxTree
43data Field rec fld = Field
44 { fget :: rec -> fld
45 , fset :: fld -> rec -> rec
46 }
48fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
49fmodify field f x = fset field (f $ fget field x) x
51instance Category Field where
52 id = Field id const
53 Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
55fgetState :: MonadState s m => Field s a -> m a
56fgetState field = gets $ fget field
58fputState :: MonadState s m => Field s a -> a -> m ()
59fputState field x = fmodifyState field (const x)
61fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
62fmodifyState field f = modify $ fmodify field f
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).
68ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
69ctxt_lookup n = Field
70 { fget = lookupCtxtExact n
71 , fset = \newVal -> case newVal of
72 Just x -> addDef n x
73 Nothing -> deleteDefExact n
74 }
76-- Maybe-lens with a default value.
77maybe_default :: a -> Field (Maybe a) a
78maybe_default dflt = Field (fromMaybe dflt) (const . Just)
81-----------------------------------
82-- Individual records and fields --
83-----------------------------------
84--
85-- These could probably be generated; let's use lazy addition for now.
86--
89-- OptInfo
90----------
92-- the optimisation record for the given (exact) name
93ist_optimisation :: Name -> Field IState OptInfo
94ist_optimisation n =
95 maybe_default Optimise
96 { inaccessible = []
97 , detaggable = False
98 }
99 . ctxt_lookup n
100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
102-- two fields of the optimisation record
103opt_inaccessible :: Field OptInfo [(Int, Name)]
104opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
106opt_detaggable :: Field OptInfo Bool
107opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
110-- CGInfo
111---------
113-- callgraph record for the given (exact) name
114ist_callgraph :: Name -> Field IState CGInfo
115ist_callgraph n =
116 maybe_default CGInfo
117 { argsdef = [], calls = [], scg = []
118 , argsused = [], usedpos = []
119 }
120 . ctxt_lookup n
121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
123-- some fields of the CGInfo record
124cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
125cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })
128-- Commandline flags
129--------------------
131opts_idrisCmdline :: Field IState [Opt]
132opts_idrisCmdline =
133 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })
134 . Field idris_options (\v ist -> ist{ idris_options = v })