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