@@ -26,57 +26,57 @@ import Util.Pretty
2626
2727
2828getContext :: Idris Context
29−getContext = do i <- get; return (tt_ctxt i)
29+getContext = do i <- getIState; return (tt_ctxt i)
3030
3131getObjectFiles :: Idris [FilePath]
32−getObjectFiles = do i <- get; return (idris_objs i)
32+getObjectFiles = do i <- getIState; return (idris_objs i)
3333
3434addObjectFile :: FilePath -> Idris ()
35−addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
35+addObjectFile f = do i <- getIState; putIState $ i { idris_objs = f : idris_objs i }
3636
3737getLibs :: Idris [String]
38−getLibs = do i <- get; return (idris_libs i)
38+getLibs = do i <- getIState; return (idris_libs i)
3939
4040addLib :: String -> Idris ()
41−addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
41+addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }
4242
4343addHdr :: String -> Idris ()
44−addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
44+addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }
4545
4646totcheck :: (FC, Name) -> Idris ()
47−totcheck n = do i <- get; put (i { idris_totcheck = idris_totcheck i ++ [n] })
47+totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
4848
4949setFlags :: Name -> [FnOpt] -> Idris ()
50−setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
50+setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
5151
5252setAccessibility :: Name -> Accessibility -> Idris ()
5353setAccessibility n a
54− = do i <- get
54+ = do i <- getIState
5555 let ctxt = setAccess n a (tt_ctxt i)
56− put (i { tt_ctxt = ctxt })
56+ putIState $ i { tt_ctxt = ctxt }
5757
5858setTotality :: Name -> Totality -> Idris ()
5959setTotality n a
60− = do i <- get
60+ = do i <- getIState
6161 let ctxt = setTotal n a (tt_ctxt i)
62− put (i { tt_ctxt = ctxt })
62+ putIState $ i { tt_ctxt = ctxt }
6363
6464getTotality :: Name -> Idris Totality
6565getTotality n
66− = do i <- get
66+ = do i <- getIState
6767 case lookupTotal n (tt_ctxt i) of
6868 [t] -> return t
6969 _ -> return (Total [])
7070
7171addToCG :: Name -> CGInfo -> Idris ()
7272addToCG n cg
73− = do i <- get
74− put (i { idris_callgraph = addDef n cg (idris_callgraph i) })
73+ = do i <- getIState
74+ putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
7575
7676addDocStr :: Name -> String -> Idris ()
7777addDocStr n doc
78− = do i <- get
79− put (i { idris_docstrings = addDef n doc (idris_docstrings i) })
78+ = do i <- getIState
79+ putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
8080
8181addToCalledG :: Name -> [Name] -> Idris ()
8282addToCalledG n ns = return () -- TODO
@@ -87,13 +87,13 @@ addToCalledG n ns = return () -- TODO
8787
8888addInstance :: Bool -> Name -> Name -> Idris ()
8989addInstance int n i
90− = do ist <- get
90+ = do ist <- getIState
9191 case lookupCtxt Nothing n (idris_classes ist) of
9292 [CI a b c d ins] ->
9393 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
94− put (ist { idris_classes = cs })
94+ putIState $ ist { idris_classes = cs }
9595 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
96− put (ist { idris_classes = cs })
96+ putIState $ ist { idris_classes = cs }
9797 where addI i ins | int = i : ins
9898 | chaser n = ins ++ [i]
9999 | otherwise = insI i ins
@@ -107,56 +107,56 @@ addInstance int n i
107107
108108addClass :: Name -> ClassInfo -> Idris ()
109109addClass n i
110− = do ist <- get
110+ = do ist <- getIState
111111 let i' = case lookupCtxt Nothing n (idris_classes ist) of
112112 [c] -> c { class_instances = class_instances i }
113113 _ -> i
114− put (ist { idris_classes = addDef n i' (idris_classes ist) })
114+ putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
115115
116116addIBC :: IBCWrite -> Idris ()
117117addIBC ibc@(IBCDef n)
118− = do i <- get
118+ = do i <- getIState
119119 when (notDef (ibc_write i)) $
120− put (i { ibc_write = ibc : ibc_write i })
120+ putIState $ i { ibc_write = ibc : ibc_write i }
121121 where notDef [] = True
122122 notDef (IBCDef n': is) | n == n' = False
123123 notDef (_ : is) = notDef is
124−addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
124+addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
125125
126126clearIBC :: Idris ()
127−clearIBC = do i <- get; put (i { ibc_write = [] })
127+clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
128128
129129getHdrs :: Idris [String]
130−getHdrs = do i <- get; return (idris_hdrs i)
130+getHdrs = do i <- getIState; return (idris_hdrs i)
131131
132132setErrLine :: Int -> Idris ()
133−setErrLine x = do i <- get;
133+setErrLine x = do i <- getIState;
134134 case (errLine i) of
135− Nothing -> put (i { errLine = Just x })
135+ Nothing -> putIState $ i { errLine = Just x }
136136 Just _ -> return ()
137137
138138clearErr :: Idris ()
139−clearErr = do i <- get
140− put (i { errLine = Nothing })
139+clearErr = do i <- getIState
140+ putIState $ i { errLine = Nothing }
141141
142142getSO :: Idris (Maybe String)
143−getSO = do i <- get
143+getSO = do i <- getIState
144144 return (compiled_so i)
145145
146146setSO :: Maybe String -> Idris ()
147−setSO s = do i <- get
148− put (i { compiled_so = s })
147+setSO s = do i <- getIState
148+ putIState $ (i { compiled_so = s })
149149
150150getIState :: Idris IState
151−getIState = get
151+getIState = lift get
152152
153153putIState :: IState -> Idris ()
154−putIState = put
154+putIState = lift . put
155155
156156getName :: Idris Int
157−getName = do i <- get;
157+getName = do i <- getIState;
158158 let idx = idris_name i;
159− put (i { idris_name = idx + 1 })
159+ putIState $ (i { idris_name = idx + 1 })
160160 return idx
161161
162162checkUndefined :: FC -> Name -> Idris ()
@@ -175,24 +175,24 @@ isUndefined fc n
175175 _ -> return True
176176
177177setContext :: Context -> Idris ()
178−setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
178+setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
179179
180180updateContext :: (Context -> Context) -> Idris ()
181−updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
181+updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
182182
183183addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
184184addConstraints fc (v, cs)
185− = do i <- get
185+ = do i <- getIState
186186 let ctxt = tt_ctxt i
187187 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
188188 next_tvar = v }
189189 let ics = zip cs (repeat fc) ++ idris_constraints i
190− put (i { tt_ctxt = ctxt', idris_constraints = ics })
190+ putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
191191
192192addDeferred :: [(Name, Type)] -> Idris ()
193193addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
194− i <- get
195− put (i { idris_metavars = map fst ns ++ idris_metavars i })
194+ i <- getIState
195+ putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
196196 where tidyNames used (Bind (MN i x) b sc)
197197 = let n' = uniqueName (UN x) used in
198198 Bind n' b $ tidyNames (n':used) sc
@@ -202,8 +202,8 @@ addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t
202202 tidyNames used b = b
203203
204204solveDeferred :: Name -> Idris ()
205−solveDeferred n = do i <- get
206− put (i { idris_metavars = idris_metavars i \\ [n] })
205+solveDeferred n = do i <- getIState
206+ putIState $ i { idris_metavars = idris_metavars i \\ [n] }
207207
208208iputStrLn :: String -> Idris ()
209209iputStrLn = liftIO . putStrLn
@@ -212,164 +212,164 @@ iWarn :: FC -> String -> Idris ()
212212iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
213213
214214setLogLevel :: Int -> Idris ()
215−setLogLevel l = do i <- get
215+setLogLevel l = do i <- getIState
216216 let opts = idris_options i
217217 let opt' = opts { opt_logLevel = l }
218− put (i { idris_options = opt' } )
218+ putIState $ i { idris_options = opt' }
219219
220220setCmdLine :: [Opt] -> Idris ()
221−setCmdLine opts = do i <- get
221+setCmdLine opts = do i <- getIState
222222 let iopts = idris_options i
223− put (i { idris_options = iopts { opt_cmdline = opts } })
223+ putIState $ i { idris_options = iopts { opt_cmdline = opts } }
224224
225225getDumpDefun :: Idris (Maybe FilePath)
226−getDumpDefun = do i <- get
226+getDumpDefun = do i <- getIState
227227 return $ findC (opt_cmdline (idris_options i))
228228 where findC [] = Nothing
229229 findC (DumpDefun x : _) = Just x
230230 findC (_ : xs) = findC xs
231231
232232getDumpCases :: Idris (Maybe FilePath)
233−getDumpCases = do i <- get
233+getDumpCases = do i <- getIState
234234 return $ findC (opt_cmdline (idris_options i))
235235 where findC [] = Nothing
236236 findC (DumpCases x : _) = Just x
237237 findC (_ : xs) = findC xs
238238
239239logLevel :: Idris Int
240−logLevel = do i <- get
240+logLevel = do i <- getIState
241241 return (opt_logLevel (idris_options i))
242242
243243setErrContext :: Bool -> Idris ()
244−setErrContext t = do i <- get
244+setErrContext t = do i <- getIState
245245 let opts = idris_options i
246246 let opt' = opts { opt_errContext = t }
247− put (i { idris_options = opt' })
247+ putIState $ i { idris_options = opt' }
248248
249249errContext :: Idris Bool
250−errContext = do i <- get
250+errContext = do i <- getIState
251251 return (opt_errContext (idris_options i))
252252
253253useREPL :: Idris Bool
254−useREPL = do i <- get
254+useREPL = do i <- getIState
255255 return (opt_repl (idris_options i))
256256
257257setREPL :: Bool -> Idris ()
258−setREPL t = do i <- get
258+setREPL t = do i <- getIState
259259 let opts = idris_options i
260260 let opt' = opts { opt_repl = t }
261− put (i { idris_options = opt' })
261+ putIState $ i { idris_options = opt' }
262262
263263setTarget :: Target -> Idris ()
264−setTarget t = do i <- get
264+setTarget t = do i <- getIState
265265 let opts = idris_options i
266266 let opt' = opts { opt_target = t }
267− put (i { idris_options = opt' })
267+ putIState $ i { idris_options = opt' }
268268
269269target :: Idris Target
270−target = do i <- get
270+target = do i <- getIState
271271 return (opt_target (idris_options i))
272272
273273setOutputTy :: OutputType -> Idris ()
274−setOutputTy t = do i <- get
274+setOutputTy t = do i <- getIState
275275 let opts = idris_options i
276276 let opt' = opts { opt_outputTy = t }
277− put (i { idris_options = opt' })
277+ putIState $ i { idris_options = opt' }
278278
279279outputTy :: Idris OutputType
280−outputTy = do i <- get
280+outputTy = do i <- getIState
281281 return $ opt_outputTy $ idris_options i
282282
283283verbose :: Idris Bool
284−verbose = do i <- get
284+verbose = do i <- getIState
285285 return (opt_verbose (idris_options i))
286286
287287setVerbose :: Bool -> Idris ()
288−setVerbose t = do i <- get
288+setVerbose t = do i <- getIState
289289 let opts = idris_options i
290290 let opt' = opts { opt_verbose = t }
291− put (i { idris_options = opt' })
291+ putIState $ i { idris_options = opt' }
292292
293293typeInType :: Idris Bool
294−typeInType = do i <- get
294+typeInType = do i <- getIState
295295 return (opt_typeintype (idris_options i))
296296
297297setTypeInType :: Bool -> Idris ()
298−setTypeInType t = do i <- get
298+setTypeInType t = do i <- getIState
299299 let opts = idris_options i
300300 let opt' = opts { opt_typeintype = t }
301− put (i { idris_options = opt' })
301+ putIState $ i { idris_options = opt' }
302302
303303coverage :: Idris Bool
304−coverage = do i <- get
304+coverage = do i <- getIState
305305 return (opt_coverage (idris_options i))
306306
307307setCoverage :: Bool -> Idris ()
308−setCoverage t = do i <- get
308+setCoverage t = do i <- getIState
309309 let opts = idris_options i
310310 let opt' = opts { opt_coverage = t }
311− put (i { idris_options = opt' })
311+ putIState $ i { idris_options = opt' }
312312
313313setIBCSubDir :: FilePath -> Idris ()
314−setIBCSubDir fp = do i <- get
314+setIBCSubDir fp = do i <- getIState
315315 let opts = idris_options i
316316 let opt' = opts { opt_ibcsubdir = fp }
317− put (i { idris_options = opt' })
317+ putIState $ i { idris_options = opt' }
318318
319319valIBCSubDir :: IState -> Idris FilePath
320320valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
321321
322322addImportDir :: FilePath -> Idris ()
323−addImportDir fp = do i <- get
323+addImportDir fp = do i <- getIState
324324 let opts = idris_options i
325325 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
326− put (i { idris_options = opt' })
326+ putIState $ i { idris_options = opt' }
327327
328328setImportDirs :: [FilePath] -> Idris ()
329−setImportDirs fps = do i <- get
329+setImportDirs fps = do i <- getIState
330330 let opts = idris_options i
331331 let opt' = opts { opt_importdirs = fps }
332− put (i { idris_options = opt' })
332+ putIState $ i { idris_options = opt' }
333333
334334allImportDirs :: IState -> Idris [FilePath]
335335allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
336336 return ("." : optdirs)
337337
338338impShow :: Idris Bool
339−impShow = do i <- get
339+impShow = do i <- getIState
340340 return (opt_showimp (idris_options i))
341341
342342setImpShow :: Bool -> Idris ()
343−setImpShow t = do i <- get
343+setImpShow t = do i <- getIState
344344 let opts = idris_options i
345345 let opt' = opts { opt_showimp = t }
346− put (i { idris_options = opt' })
346+ putIState $ i { idris_options = opt' }
347347
348348logLvl :: Int -> String -> Idris ()
349−logLvl l str = do i <- get
349+logLvl l str = do i <- getIState
350350 let lvl = opt_logLevel (idris_options i)
351351 when (lvl >= l)
352352 $ do liftIO (putStrLn str)
353− put (i { idris_log = idris_log i ++ str ++ "\n" } )
353+ putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
354354
355355cmdOptType :: Opt -> Idris Bool
356−cmdOptType x = do i <- get
356+cmdOptType x = do i <- getIState
357357 return $ x `elem` opt_cmdline (idris_options i)
358358
359359iLOG :: String -> Idris ()
360360iLOG = logLvl 1
361361
362362noErrors :: Idris Bool
363−noErrors = do i <- get
363+noErrors = do i <- getIState
364364 case errLine i of
365365 Nothing -> return True
366366 _ -> return False
367367
368368setTypeCase :: Bool -> Idris ()
369−setTypeCase t = do i <- get
369+setTypeCase t = do i <- getIState
370370 let opts = idris_options i
371371 let opt' = opts { opt_typecase = t }
372− put (i { idris_options = opt' })
372+ putIState $ i { idris_options = opt' }
373373
374374
375375-- For inferring types of things
@@ -634,8 +634,8 @@ addStatics n tm ptm =
634634 let statics' = nub $ map fst statics ++
635635 filter (\x -> not (elem x dnames)) stnames
636636 let stpos = staticList statics' tm
637− i <- get
638− put (i { idris_statics = addDef n stpos (idris_statics i) })
637+ i <- getIState
638+ putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
639639 addIBC (IBCStatic n)
640640 where
641641 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
@@ -659,14 +659,14 @@ implicit syn n ptm = implicit' syn [] n ptm
659659
660660implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
661661implicit' syn ignore n ptm
662− = do i <- get
662+ = do i <- getIState
663663 let (tm', impdata) = implicitise syn ignore i ptm
664664-- let (tm'', spos) = findStatics i tm'
665− put (i { idris_implicits = addDef n impdata (idris_implicits i) })
665+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
666666 addIBC (IBCImp n)
667667 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
668668-- i <- get
669−-- put (i { idris_statics = addDef n spos (idris_statics i) })
669+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
670670 return tm'
671671
672672implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])