git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/ASTUtils.hs
167 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.
5Copyright :
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.Applicative
56import Control.Category
57import Control.Monad.State.Class
58import Data.Maybe
60data Field rec fld = Field
61 { fget :: rec -> fld
62 , fset :: fld -> rec -> rec
63 }
65fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
66fmodify field f x = fset field (f $ fget field x) x
68instance Category Field where
69 id = Field id const
70 Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
72fgetState :: MonadState s m => Field s a -> m a
73fgetState field = gets $ fget field
75fputState :: MonadState s m => Field s a -> a -> m ()
76fputState field x = fmodifyState field (const x)
78fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
79fmodifyState field f = modify $ fmodify field f
81-- | Exact-name context lookup; uses Nothing for deleted values
82-- (read+write!).
83--
84-- Reading a non-existing value yields Nothing,
85-- writing Nothing deletes the value (if it existed).
86ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
87ctxt_lookup n = Field
88 { fget = lookupCtxtExact n
89 , fset = \newVal -> case newVal of
90 Just x -> addDef n x
91 Nothing -> deleteDefExact n
92 }
94-- Maybe-lens with a default value.
95maybe_default :: a -> Field (Maybe a) a
96maybe_default dflt = Field (fromMaybe dflt) (const . Just)
99-----------------------------------
100-- Individual records and fields --
101-----------------------------------
102--
103-- These could probably be generated; let's use lazy addition for now.
104--
107-- OptInfo
108----------
110-- | the optimisation record for the given (exact) name
111ist_optimisation :: Name -> Field IState OptInfo
112ist_optimisation n =
113 maybe_default Optimise
114 { inaccessible = []
115 , detaggable = False
116 , forceable = []
117 }
118 . ctxt_lookup n
119 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
121-- | two fields of the optimisation record
122opt_inaccessible :: Field OptInfo [(Int, Name)]
123opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
125opt_detaggable :: Field OptInfo Bool
126opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
128opt_forceable :: Field OptInfo [Int]
129opt_forceable = Field forceable (\v opt -> opt{ forceable = v })
131-- | callgraph record for the given (exact) name
132ist_callgraph :: Name -> Field IState CGInfo
133ist_callgraph n =
134 maybe_default CGInfo
135 { calls = [], allCalls = Nothing, scg = [], usedpos = []
136 }
137 . ctxt_lookup n
138 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
140cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
141cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })
143-- | Commandline flags
144opts_idrisCmdline :: Field IState [Opt]
145opts_idrisCmdline =
146 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })
147 . Field idris_options (\v ist -> ist{ idris_options = v })
149-- | TT Context
150--
151-- This has a terrible name, but I'm not sure of a better one that
152-- isn't confusingly close to tt_ctxt
153known_terms :: Field IState (Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))
154known_terms = Field (definitions . tt_ctxt)
155 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
157known_interfaces :: Field IState (Ctxt InterfaceInfo)
158known_interfaces = Field idris_interfaces (\v state -> state {idris_interfaces = idris_interfaces state})
161-- | Names defined at the repl
162repl_definitions :: Field IState [Name]
163repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})
165-- | Fixity declarations in an IState
166idris_fixities :: Field IState [FixDecl]
167idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})