git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/ASTUtils.hs
115 lines 3.5 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 typeclass InitialValue.
30import Control.Category
31import Control.Applicative
32import Control.Monad.State.Class
33import Data.Maybe
34import Prelude hiding (id, (.))
36import Idris.Core.TT
37import Idris.AbsSyntaxTree
39data Field rec fld = Field
40 { fget :: rec -> fld
41 , fset :: fld -> rec -> rec
42 }
44fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
45fmodify field f x = fset field (f $ fget field x) x
47instance Category Field where
48 id = Field id const
49 Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
51fgetState :: MonadState s m => Field s a -> m a
52fgetState field = gets $ fget field
54fputState :: MonadState s m => Field s a -> a -> m ()
55fputState field x = fmodifyState field (const x)
57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
58fmodifyState 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.
62--
63-- This class formalises the notion of an initial value for a record.
64class InitialValue a where
65 initialValue :: a
67-- Exact-name context lookup; uses the initial value if needed.
68ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
69ctxt_lookupExact n = Field
70 { fget = fromMaybe initialValue . lookupCtxtExact n
71 , fset = addDef n
72 }
75-----------------------------------
76-- Individual records and fields --
77-----------------------------------
78--
79-- These could probably be generated; let's use lazy addition for now.
80--
83-- OptInfo
84----------
86instance InitialValue OptInfo where
87 initialValue = Optimise [] False
89-- the optimisation record for the given (exact) name
90ist_optimisation :: Name -> Field IState OptInfo
91ist_optimisation n = ctxt_lookupExact n
92 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
94-- two fields of the optimisation record
95opt_inaccessible :: Field OptInfo [(Int, Name)]
96opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
98opt_detaggable :: Field OptInfo Bool
99opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
102-- CGInfo
103---------
105instance InitialValue CGInfo where
106 initialValue = CGInfo [] [] [] [] []
108-- callgraph record for the given (exact) name
109ist_callgraph :: Name -> Field IState CGInfo
110ist_callgraph n = ctxt_lookupExact n
111 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
113-- some fields of the CGInfo record
114cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
115cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })