053708a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #176 from david-christiansen/completion

053708aEdwin Brady14 years ago

src/Core/ProofShell.hs+3−1

compare with master

unifiedsplit

@@ -11,6 +11,8 @@ import Core.Elaborate

11import Control.Monad.State

12import System.Console.Haskeline

14+import Idris.AbsSyntaxTree (Idris)

15+

14import Util.Pretty

16import Util.Pretty

16data ShellState = ShellState

18data ShellState = ShellState

@@ -55,7 +57,7 @@ processCommand (Tac e) state

55 err -> (state, show err)

57 err -> (state, show err)

56 | otherwise = (state, "No proof in progress")

58 | otherwise = (state, "No proof in progress")

58−runShell :: ShellState -> InputT IO ShellState

60+runShell :: ShellState -> Idris ShellState

59runShell st = do (prompt, parser) <-

61runShell st = do (prompt, parser) <-

60 maybe (return ("TT# ", parseCommand))

62 maybe (return ("TT# ", parseCommand))

61 (\st -> do outputStrLn . render . pretty $ st

63 (\st -> do outputStrLn . render . pretty $ st

src/IRTS/Compiler.hs+3−3

@@ -73,7 +73,7 @@ compile target f tm

73 Bytecode -> liftIO $ dumpBC c f

74 ToJavaScript -> liftIO $ codegenJavaScript c f outty

75 Error e -> fail $ show e

76− where checkMVs = do i <- get

76+ where checkMVs = do i <- getIState

77 case idris_metavars i \\ primDefs of

78 [] -> return ()

79 ms -> fail $ "There are undefined metavariables: " ++ show ms

@@ -91,7 +91,7 @@ irMain tm = do i <- ir tm

92allNames :: [Name] -> Name -> Idris [Name]

93allNames ns n | n `elem` ns = return []

94−allNames ns n = do i <- get

94+allNames ns n = do i <- getIState

95 case lookupCtxt Nothing n (idris_callgraph i) of

96 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

97 return (nub (n : concat more))

@@ -193,7 +193,7 @@ instance ToIR (TT Name) where

193 | (P (DCon t a) n _, args) <- unApply tm

194 = irCon env t a n args

195 | (P _ n _, args) <- unApply tm

196− = do i <- get

196+ = do i <- getIState

197 args' <- mapM (ir' env) args

198 case getPrim i n args' of

199 Just tm -> return tm

src/Idris/AbsSyntax.hs+94−94

@@ -26,57 +26,57 @@ import Util.Pretty

28getContext :: Idris Context

29−getContext = do i <- get; return (tt_ctxt i)

29+getContext = do i <- getIState; return (tt_ctxt i)

31getObjectFiles :: Idris [FilePath]

32−getObjectFiles = do i <- get; return (idris_objs i)

32+getObjectFiles = do i <- getIState; return (idris_objs i)

34addObjectFile :: 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 }

37getLibs :: Idris [String]

38−getLibs = do i <- get; return (idris_libs i)

38+getLibs = do i <- getIState; return (idris_libs i)

40addLib :: 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 }

43addHdr :: 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 }

46totcheck :: (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] }

49setFlags :: 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) }

52setAccessibility :: Name -> Accessibility -> Idris ()

53setAccessibility n a

54− = do i <- get

54+ = do i <- getIState

55 let ctxt = setAccess n a (tt_ctxt i)

56− put (i { tt_ctxt = ctxt })

56+ putIState $ i { tt_ctxt = ctxt }

58setTotality :: Name -> Totality -> Idris ()

59setTotality n a

60− = do i <- get

60+ = do i <- getIState

61 let ctxt = setTotal n a (tt_ctxt i)

62− put (i { tt_ctxt = ctxt })

62+ putIState $ i { tt_ctxt = ctxt }

64getTotality :: Name -> Idris Totality

65getTotality n

66− = do i <- get

66+ = do i <- getIState

67 case lookupTotal n (tt_ctxt i) of

68 [t] -> return t

69 _ -> return (Total [])

71addToCG :: Name -> CGInfo -> Idris ()

72addToCG n cg

73− = do i <- get

73+ = do i <- getIState

74− put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

74+ putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

76addDocStr :: Name -> String -> Idris ()

77addDocStr n doc

78− = do i <- get

78+ = do i <- getIState

79− put (i { idris_docstrings = addDef n doc (idris_docstrings i) })

79+ putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }

81addToCalledG :: Name -> [Name] -> Idris ()

82addToCalledG n ns = return () -- TODO

@@ -87,13 +87,13 @@ addToCalledG n ns = return () -- TODO

88addInstance :: Bool -> Name -> Name -> Idris ()

89addInstance int n i

90− = do ist <- get

90+ = do ist <- getIState

91 case lookupCtxt Nothing n (idris_classes ist) of

92 [CI a b c d ins] ->

93 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 }

95 _ -> 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 }

97 where addI i ins | int = i : ins

98 | chaser n = ins ++ [i]

99 | otherwise = insI i ins

@@ -107,56 +107,56 @@ addInstance int n i

107

108addClass :: Name -> ClassInfo -> Idris ()

109addClass n i

110− = do ist <- get

110+ = do ist <- getIState

111 let i' = case lookupCtxt Nothing n (idris_classes ist) of

112 [c] -> c { class_instances = class_instances i }

113 _ -> i

114− put (ist { idris_classes = addDef n i' (idris_classes ist) })

114+ putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

115

116addIBC :: IBCWrite -> Idris ()

117addIBC ibc@(IBCDef n)

118− = do i <- get

118+ = do i <- getIState

119 when (notDef (ibc_write i)) $

120− put (i { ibc_write = ibc : ibc_write i })

120+ putIState $ i { ibc_write = ibc : ibc_write i }

121 where notDef [] = True

122 notDef (IBCDef n': is) | n == n' = False

123 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 }

125

126clearIBC :: Idris ()

127−clearIBC = do i <- get; put (i { ibc_write = [] })

127+clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

128

129getHdrs :: Idris [String]

130−getHdrs = do i <- get; return (idris_hdrs i)

130+getHdrs = do i <- getIState; return (idris_hdrs i)

131

132setErrLine :: Int -> Idris ()

133−setErrLine x = do i <- get;

133+setErrLine x = do i <- getIState;

134 case (errLine i) of

135− Nothing -> put (i { errLine = Just x })

135+ Nothing -> putIState $ i { errLine = Just x }

136 Just _ -> return ()

137

138clearErr :: Idris ()

139−clearErr = do i <- get

139+clearErr = do i <- getIState

140− put (i { errLine = Nothing })

140+ putIState $ i { errLine = Nothing }

141

142getSO :: Idris (Maybe String)

143−getSO = do i <- get

143+getSO = do i <- getIState

144 return (compiled_so i)

145

146setSO :: Maybe String -> Idris ()

147−setSO s = do i <- get

147+setSO s = do i <- getIState

148− put (i { compiled_so = s })

148+ putIState $ (i { compiled_so = s })

149

150getIState :: Idris IState

151−getIState = get

151+getIState = lift get

152

153putIState :: IState -> Idris ()

154−putIState = put

154+putIState = lift . put

155

156getName :: Idris Int

157−getName = do i <- get;

157+getName = do i <- getIState;

158 let idx = idris_name i;

159− put (i { idris_name = idx + 1 })

159+ putIState $ (i { idris_name = idx + 1 })

160 return idx

161

162checkUndefined :: FC -> Name -> Idris ()

@@ -175,24 +175,24 @@ isUndefined fc n

175 _ -> return True

176

177setContext :: Context -> Idris ()

178−setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

178+setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )

179

180updateContext :: (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) } )

182

183addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

184addConstraints fc (v, cs)

185− = do i <- get

185+ = do i <- getIState

186 let ctxt = tt_ctxt i

187 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,

188 next_tvar = v }

189 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 }

191

192addDeferred :: [(Name, Type)] -> Idris ()

193addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns

194− i <- get

194+ i <- getIState

195− put (i { idris_metavars = map fst ns ++ idris_metavars i })

195+ putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

196 where tidyNames used (Bind (MN i x) b sc)

197 = let n' = uniqueName (UN x) used in

198 Bind n' b $ tidyNames (n':used) sc

@@ -202,8 +202,8 @@ addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t

202 tidyNames used b = b

203

204solveDeferred :: Name -> Idris ()

205−solveDeferred n = do i <- get

205+solveDeferred n = do i <- getIState

206− put (i { idris_metavars = idris_metavars i \\ [n] })

206+ putIState $ i { idris_metavars = idris_metavars i \\ [n] }

207

208iputStrLn :: String -> Idris ()

209iputStrLn = liftIO . putStrLn

@@ -212,164 +212,164 @@ iWarn :: FC -> String -> Idris ()

212iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)

213

214setLogLevel :: Int -> Idris ()

215−setLogLevel l = do i <- get

215+setLogLevel l = do i <- getIState

216 let opts = idris_options i

217 let opt' = opts { opt_logLevel = l }

218− put (i { idris_options = opt' } )

218+ putIState $ i { idris_options = opt' }

219

220setCmdLine :: [Opt] -> Idris ()

221−setCmdLine opts = do i <- get

221+setCmdLine opts = do i <- getIState

222 let iopts = idris_options i

223− put (i { idris_options = iopts { opt_cmdline = opts } })

223+ putIState $ i { idris_options = iopts { opt_cmdline = opts } }

224

225getDumpDefun :: Idris (Maybe FilePath)

226−getDumpDefun = do i <- get

226+getDumpDefun = do i <- getIState

227 return $ findC (opt_cmdline (idris_options i))

228 where findC [] = Nothing

229 findC (DumpDefun x : _) = Just x

230 findC (_ : xs) = findC xs

231

232getDumpCases :: Idris (Maybe FilePath)

233−getDumpCases = do i <- get

233+getDumpCases = do i <- getIState

234 return $ findC (opt_cmdline (idris_options i))

235 where findC [] = Nothing

236 findC (DumpCases x : _) = Just x

237 findC (_ : xs) = findC xs

238

239logLevel :: Idris Int

240−logLevel = do i <- get

240+logLevel = do i <- getIState

241 return (opt_logLevel (idris_options i))

242

243setErrContext :: Bool -> Idris ()

244−setErrContext t = do i <- get

244+setErrContext t = do i <- getIState

245 let opts = idris_options i

246 let opt' = opts { opt_errContext = t }

247− put (i { idris_options = opt' })

247+ putIState $ i { idris_options = opt' }

248

249errContext :: Idris Bool

250−errContext = do i <- get

250+errContext = do i <- getIState

251 return (opt_errContext (idris_options i))

252

253useREPL :: Idris Bool

254−useREPL = do i <- get

254+useREPL = do i <- getIState

255 return (opt_repl (idris_options i))

256

257setREPL :: Bool -> Idris ()

258−setREPL t = do i <- get

258+setREPL t = do i <- getIState

259 let opts = idris_options i

260 let opt' = opts { opt_repl = t }

261− put (i { idris_options = opt' })

261+ putIState $ i { idris_options = opt' }

262

263setTarget :: Target -> Idris ()

264−setTarget t = do i <- get

264+setTarget t = do i <- getIState

265 let opts = idris_options i

266 let opt' = opts { opt_target = t }

267− put (i { idris_options = opt' })

267+ putIState $ i { idris_options = opt' }

268

269target :: Idris Target

270−target = do i <- get

270+target = do i <- getIState

271 return (opt_target (idris_options i))

272

273setOutputTy :: OutputType -> Idris ()

274−setOutputTy t = do i <- get

274+setOutputTy t = do i <- getIState

275 let opts = idris_options i

276 let opt' = opts { opt_outputTy = t }

277− put (i { idris_options = opt' })

277+ putIState $ i { idris_options = opt' }

278

279outputTy :: Idris OutputType

280−outputTy = do i <- get

280+outputTy = do i <- getIState

281 return $ opt_outputTy $ idris_options i

282

283verbose :: Idris Bool

284−verbose = do i <- get

284+verbose = do i <- getIState

285 return (opt_verbose (idris_options i))

286

287setVerbose :: Bool -> Idris ()

288−setVerbose t = do i <- get

288+setVerbose t = do i <- getIState

289 let opts = idris_options i

290 let opt' = opts { opt_verbose = t }

291− put (i { idris_options = opt' })

291+ putIState $ i { idris_options = opt' }

292

293typeInType :: Idris Bool

294−typeInType = do i <- get

294+typeInType = do i <- getIState

295 return (opt_typeintype (idris_options i))

296

297setTypeInType :: Bool -> Idris ()

298−setTypeInType t = do i <- get

298+setTypeInType t = do i <- getIState

299 let opts = idris_options i

300 let opt' = opts { opt_typeintype = t }

301− put (i { idris_options = opt' })

301+ putIState $ i { idris_options = opt' }

302

303coverage :: Idris Bool

304−coverage = do i <- get

304+coverage = do i <- getIState

305 return (opt_coverage (idris_options i))

306

307setCoverage :: Bool -> Idris ()

308−setCoverage t = do i <- get

308+setCoverage t = do i <- getIState

309 let opts = idris_options i

310 let opt' = opts { opt_coverage = t }

311− put (i { idris_options = opt' })

311+ putIState $ i { idris_options = opt' }

312

313setIBCSubDir :: FilePath -> Idris ()

314−setIBCSubDir fp = do i <- get

314+setIBCSubDir fp = do i <- getIState

315 let opts = idris_options i

316 let opt' = opts { opt_ibcsubdir = fp }

317− put (i { idris_options = opt' })

317+ putIState $ i { idris_options = opt' }

318

319valIBCSubDir :: IState -> Idris FilePath

320valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

321

322addImportDir :: FilePath -> Idris ()

323−addImportDir fp = do i <- get

323+addImportDir fp = do i <- getIState

324 let opts = idris_options i

325 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }

326− put (i { idris_options = opt' })

326+ putIState $ i { idris_options = opt' }

327

328setImportDirs :: [FilePath] -> Idris ()

329−setImportDirs fps = do i <- get

329+setImportDirs fps = do i <- getIState

330 let opts = idris_options i

331 let opt' = opts { opt_importdirs = fps }

332− put (i { idris_options = opt' })

332+ putIState $ i { idris_options = opt' }

333

334allImportDirs :: IState -> Idris [FilePath]

335allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

336 return ("." : optdirs)

337

338impShow :: Idris Bool

339−impShow = do i <- get

339+impShow = do i <- getIState

340 return (opt_showimp (idris_options i))

341

342setImpShow :: Bool -> Idris ()

343−setImpShow t = do i <- get

343+setImpShow t = do i <- getIState

344 let opts = idris_options i

345 let opt' = opts { opt_showimp = t }

346− put (i { idris_options = opt' })

346+ putIState $ i { idris_options = opt' }

347

348logLvl :: Int -> String -> Idris ()

349−logLvl l str = do i <- get

349+logLvl l str = do i <- getIState

350 let lvl = opt_logLevel (idris_options i)

351 when (lvl >= l)

352 $ do liftIO (putStrLn str)

353− put (i { idris_log = idris_log i ++ str ++ "\n" } )

353+ putIState $ i { idris_log = idris_log i ++ str ++ "\n" }

354

355cmdOptType :: Opt -> Idris Bool

356−cmdOptType x = do i <- get

356+cmdOptType x = do i <- getIState

357 return $ x `elem` opt_cmdline (idris_options i)

358

359iLOG :: String -> Idris ()

360iLOG = logLvl 1

361

362noErrors :: Idris Bool

363−noErrors = do i <- get

363+noErrors = do i <- getIState

364 case errLine i of

365 Nothing -> return True

366 _ -> return False

367

368setTypeCase :: Bool -> Idris ()

369−setTypeCase t = do i <- get

369+setTypeCase t = do i <- getIState

370 let opts = idris_options i

371 let opt' = opts { opt_typecase = t }

372− put (i { idris_options = opt' })

372+ putIState $ i { idris_options = opt' }

373

374

375-- For inferring types of things

@@ -634,8 +634,8 @@ addStatics n tm ptm =

634 let statics' = nub $ map fst statics ++

635 filter (\x -> not (elem x dnames)) stnames

636 let stpos = staticList statics' tm

637− i <- get

637+ i <- getIState

638− put (i { idris_statics = addDef n stpos (idris_statics i) })

638+ putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

639 addIBC (IBCStatic n)

640 where

641 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)

@@ -659,14 +659,14 @@ implicit syn n ptm = implicit' syn [] n ptm

659

660implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

661implicit' syn ignore n ptm

662− = do i <- get

662+ = do i <- getIState

663 let (tm', impdata) = implicitise syn ignore i ptm

664-- 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) }

666 addIBC (IBCImp n)

667 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

668-- i <- get

669−-- put (i { idris_statics = addDef n spos (idris_statics i) })

669+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

670 return tm'

671

672implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

src/Idris/AbsSyntaxTree.hs+1−1

@@ -136,7 +136,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

136

137-- The monad for the main REPL - reading and processing files and updating

138-- global state (hence the IO inner monad).

139−type Idris = StateT IState (InputT IO)

139+type Idris = InputT (StateT IState IO)

140

141-- Commands in the REPL

142

src/Idris/Coverage.hs+9−9

@@ -33,23 +33,23 @@ genMissing fn args sc

33-- covering...)

35mkPatTm :: PTerm -> Idris Term

36−mkPatTm t = do i <- get

36+mkPatTm t = do i <- getIState

37 let timp = addImpl' True [] [] i t

38 evalStateT (toTT timp) 0

39 where

40− toTT (PRef _ n) = do i <- lift $ get

40+ toTT (PRef _ n) = do i <- lift getIState

41 case lookupDef Nothing n (tt_ctxt i) of

42 [TyDecl nt _] -> return $ P nt n Erased

43 _ -> return $ P Ref n Erased

44 toTT (PApp _ t args) = do t' <- toTT t

45 args' <- mapM (toTT . getTm) args

46 return $ mkApp t' args'

47− toTT _ = do v <- get

47+ toTT _ = do v <- get

48 put (v + 1)

49 return (P Bound (MN v "imp") Erased)

51mkPTerm :: Name -> [TT Name] -> Idris PTerm

52−mkPTerm f args = do i <- get

52+mkPTerm f args = do i <- getIState

53 let fapp = mkApp (P Bound f Erased) (map eraseName args)

54 return $ delab i fapp

55 where eraseName (App f a) = App (eraseName f) (eraseName a)

@@ -90,7 +90,7 @@ dropDefault (c : cs) = c : dropDefault cs

90dropDefault [] = []

92expandTree :: SC -> Idris SC

93−expandTree (Case n alts) = do i <- get

93+expandTree (Case n alts) = do i <- getIState

94 as <- expandAlts i (dropDefault alts)

95 (getDefault alts)

96 alts' <- mapM expandTreeA as

@@ -307,7 +307,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

307calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]

308 -> Idris Totality

309calcTotality path fc n pats

310− = do i <- get

310+ = do i <- getIState

311 let opts = case lookupCtxt Nothing n (idris_flags i) of

312 [fs] -> fs

313 _ -> []

@@ -370,7 +370,7 @@ checkTotality path fc n

370 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

371

372 warnPartial n t

373− = do i <- get

373+ = do i <- getIState

374 case lookupDef Nothing n (tt_ctxt i) of

375 [x] -> do

376 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

@@ -399,7 +399,7 @@ checkDeclTotality (fc, n)

399

400buildSCG :: (FC, Name) -> Idris ()

401buildSCG (_, n) = do

402− ist <- get

402+ ist <- getIState

403 case lookupCtxt Nothing n (idris_callgraph ist) of

404 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of

405 [CaseOp _ _ _ _ _ args sc _ _] ->

@@ -495,7 +495,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

495

496checkSizeChange :: Name -> Idris Totality

497checkSizeChange n = do

498− ist <- get

498+ ist <- getIState

499 case lookupCtxt Nothing n (idris_callgraph ist) of

500 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

501 logLvl 6 ("Multipath for " ++ show n ++ ":\n" ++

src/Idris/ElabDecls.hs+39−39

@@ -44,7 +44,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

44 n = liftname info n_in in -}

45 do checkUndefined fc n

46 ctxt <- getContext

47− i <- get

47+ i <- getIState

48 logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'

49 ty' <- implicit syn n ty'

50 let ty = addImpl i ty'

@@ -91,7 +91,7 @@ elabPostulate info syn doc fc opts n ty

91 fty <- case lookupTy Nothing n ctxt of

92 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

93 [ty] -> return ty

94− ist <- get

94+ ist <- getIState

95 let (ap, _) = unApply (getRetTy fty)

96 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

97 let postOK = case ap of

@@ -110,7 +110,7 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

110 = do iLOG (show (fc, doc))

111 checkUndefined fc n

112 ctxt <- getContext

113− i <- get

113+ i <- getIState

114 t_in <- implicit syn n t_in

115 let t = addImpl i t_in

116 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -126,7 +126,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

126 = do iLOG (show fc)

127 undef <- isUndefined fc n

128 ctxt <- getContext

129− i <- get

129+ i <- getIState

130 t_in <- implicit syn n t_in

131 let t = addImpl i t_in

132 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -140,11 +140,11 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

140 when undef $ updateContext (addTyDecl n cty)

141 cons <- mapM (elabCon info syn n codata) dcons

142 ttag <- getName

143− i <- get

143+ i <- getIState

144 let as = map (const Nothing) (getArgTys cty)

145 let params = findParams (zip as (repeat True)) (map snd cons)

146 logLvl 2 $ "Parameters : " ++ show params

147− put (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

147+ putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

148 (idris_datatypes i) })

149 addIBC (IBCDef n)

150 addIBC (IBCData n)

@@ -188,7 +188,7 @@ elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

188elabRecord info syn doc fc tyn ty cdoc cn cty

189 = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

190 cty' <- implicit syn cn cty

191− i <- get

191+ i <- getIState

192 cty <- case lookupTy Nothing cn (tt_ctxt i) of

193 [t] -> return (delab i t)

194 _ -> fail "Something went inexplicably wrong"

@@ -213,13 +213,13 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

213 isNonImp _ = Nothing

214

215 tryElabDecl info (fn, ty, val)

216− = do i <- get

216+ = do i <- getIState

217 idrisCatch (do elabDecl' EAll info ty

218 elabDecl' EAll info val)

219 (\v -> do iputStrLn $ show fc ++

220 ":Warning - can't generate setter for " ++

221 show fn ++ " (" ++ show ty ++ ")"

222− put i)

222+ putIState i)

223

224 getImplB k (PPi (Imp l s _) n Placeholder sc)

225 = getImplB k sc

@@ -297,7 +297,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

297elabCon info syn tn codata (doc, n, t_in, fc)

298 = do checkUndefined fc n

299 ctxt <- getContext

300− i <- get

300+ i <- getIState

301 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

302 let t = addImpl i t_in

303 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

@@ -343,7 +343,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

343 (zip [0..] cs)

344 -- if the return type of 'ty' is collapsible, the optimised version should

345 -- just do nothing

346− ist <- get

346+ ist <- getIState

347 let (ap, _) = unApply (getRetTy fty)

348 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

349 -- FIXME: Really ought to only do this for total functions!

@@ -354,17 +354,17 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

354 _ -> False

355 _ -> False

356 solveDeferred n

357− ist <- get

357+ ist <- getIState

358 when doNothing $

359 case lookupCtxt Nothing n (idris_optimisation ist) of

360 [oi] -> do let opts = addDef n (oi { collapsible = True })

361 (idris_optimisation ist)

362− put (ist { idris_optimisation = opts })

362+ putIState (ist { idris_optimisation = opts })

363 _ -> do let opts = addDef n (Optimise True [] [])

364 (idris_optimisation ist)

365− put (ist { idris_optimisation = opts })

365+ putIState (ist { idris_optimisation = opts })

366 addIBC (IBCOpt n)

367− ist <- get

367+ ist <- getIState

368 let pats = pats_in

369 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

370 -- show l ++ " = " ++

@@ -401,7 +401,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

401 pdef' <- applyOpts optpdef

402 logLvl 2 $ "Optimised patterns"

403 logLvl 5 $ show pdef'

404− ist <- get

404+ ist <- getIState

405 -- let wf = wellFounded ist n sc

406 let tot = if pcover || AssertTotal `elem` opts

407 then Unchecked -- finish checking later

@@ -425,8 +425,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

425 logLvl 3 (show tree)

426 logLvl 3 $ "Optimised: " ++ show tree'

427 ctxt <- getContext

428− ist <- get

428+ ist <- getIState

429− put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

429+ putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

430 case lookupTy (namespace info) n ctxt of

431 [ty] -> do updateContext (addCasedef n (inlinable opts)

432 tcase knowncovering

@@ -437,7 +437,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

437 setTotality n tot

438 totcheck (fc, n)

439 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

440− i <- get

440+ i <- getIState

441 case lookupDef Nothing n (tt_ctxt i) of

442 (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

443 do let calls = findCalls sc' scargs'

@@ -485,7 +485,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

485elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

486elabVal info aspat tm_in

487 = do ctxt <- getContext

488− i <- get

488+ i <- getIState

489 let tm = addImpl i tm_in

490 logLvl 10 (showImp True tm)

491 -- try:

@@ -510,7 +510,7 @@ elabVal info aspat tm_in

510checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

511checkPossible info fc tcgen fname lhs_in

512 = do ctxt <- getContext

513− i <- get

513+ i <- getIState

514 let lhs = addImpl i lhs_in

515 -- if the LHS type checks, it is possible

516 case elaborate ctxt (MN 0 "patLHS") infP []

@@ -537,7 +537,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

537 = do ctxt <- getContext

538 -- Build the LHS as an "Infer", and pull out its type and

539 -- pattern bindings

540− i <- get

540+ i <- getIState

541 -- get the parameters first, to pass through to any where block

542 let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of

543 [t] -> t

@@ -575,7 +575,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

575 logLvl 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

576 mapM_ (elabDecl' EAll info) wbefore

577 -- Now build the RHS, using the type of the LHS as the goal.

578− i <- get -- new implicits from where block

578+ i <- getIState -- new implicits from where block

579 logLvl 5 (showImp True (expandParams decorate newargs defs (defs \\ decls) rhs_in))

580 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

581 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

@@ -609,7 +609,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

609 case converts ctxt [] clhsty crhsty of

610 OK _ -> return ()

611 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

612− i <- get

612+ i <- getIState

613 checkInferred fc (delab' i crhs True) rhs

614 return $ Right (clhs, crhs)

615 where

@@ -678,7 +678,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

678 = do ctxt <- getContext

679 -- Build the LHS as an "Infer", and pull out its type and

680 -- pattern bindings

681− i <- get

681+ i <- getIState

682 let lhs = addImpl i lhs_in

683 logLvl 5 ("LHS: " ++ showImp True lhs)

684 ((lhs', dlhs, []), _) <-

@@ -731,7 +731,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

731 logLvl 3 ("New function type " ++ show wtype)

732 let wname = MN windex (show fname)

733 let imps = getImps wtype -- add to implicits context

734− put (i { idris_implicits = addDef wname imps (idris_implicits i) })

734+ putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

735 addIBC (IBCDef wname)

736 def' <- checkDef fc [(wname, wtype)]

737 addDeferred def'

@@ -751,7 +751,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

751 (map (pexp . (PRef fc) . fst) bargs_post))

752 logLvl 5 ("New RHS " ++ showImp True rhs)

753 ctxt <- getContext -- New context with block added

754− i <- get

754+ i <- getIState

755 ((rhs', defer, is), _) <-

756 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

757 (do pbinds lhs_tm

@@ -776,7 +776,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

776 mkAuxC wname lhs ns ns' d = return $ d

777

778 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

779− = do i <- get

779+ = do i <- getIState

780 let tm = addImpl i tm_in

781 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

782 showImp True toplhs)

@@ -787,7 +787,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

787 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

788 return $ PClause fc wname lhs ws rhs wheres

789 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

790− = do i <- get

790+ = do i <- getIState

791 let tm = addImpl i tm_in

792 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

793 showImp True toplhs)

@@ -864,7 +864,7 @@ elabClass info syn doc fc constraints tn ps ds

864 mapM_ (elabDecl EAll info) (concat fns)

865 -- add the default definitions

866 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

867− i <- get

867+ i <- getIState

868 addIBC (IBCClass tn)

869 where

870 nodoc (n, (_, o, t)) = (n, (o, t))

@@ -918,7 +918,7 @@ elabClass info syn doc fc constraints tn ps ds

918 let ty = PPi constraint (MN 0 "pc") c con

919 iLOG (showImp True ty)

920 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

921− i <- get

921+ i <- getIState

922 let conn = case con of

923 PRef _ n -> n

924 PApp _ (PRef _ n) _ -> n

@@ -982,7 +982,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

982 Maybe Name -> -- explicit name

983 [PDecl] -> Idris ()

984elabInstance info syn fc cs n ps t expn ds

985− = do i <- get

985+ = do i <- getIState

986 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

987 [c] -> return c

988 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

@@ -1137,7 +1137,7 @@ elabInstance info syn fc cs n ps t expn ds

1137 let ty = PPi constraint (MN 0 "pc") c con

1138 iLOG (showImp True ty)

1139 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

1140− i <- get

1140+ i <- getIState

1141 let conn = case con of

1142 PRef _ n -> n

1143 PApp _ (PRef _ n) _ -> n

@@ -1214,7 +1214,7 @@ elabDecl' what info (PData doc s f co d)

1214elabDecl' what info d@(PClauses f o n ps)

1215 | what /= ETypes

1216 = do iLOG $ "Elaborating clause " ++ show n

1217− i <- get -- get the type options too

1217+ i <- getIState -- get the type options too

1218 let o' = case lookupCtxt Nothing n (idris_flags i) of

1219 [fs] -> fs

1220 [] -> []

@@ -1223,7 +1223,7 @@ elabDecl' what info (PMutual f ps)

1223 = do mapM_ (elabDecl ETypes info) ps

1224 mapM_ (elabDecl EDefns info) ps

1225elabDecl' what info (PParams f ns ps)

1226− = do i <- get

1226+ = do i <- getIState

1227 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++

1228 show (concatMap tldeclared ps)

1229 let nblock = pblock i

@@ -1256,8 +1256,8 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

1256 = do iLOG $ "Elaborating record " ++ show tyn

1257 elabRecord info s doc f tyn ty cdoc cn cty

1258elabDecl' _ info (PDSL n dsl)

1259− = do i <- get

1259+ = do i <- getIState

1260− put (i { idris_dsls = addDef n dsl (idris_dsls i) })

1260+ putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

1261 addIBC (IBCDSL n)

1262elabDecl' what info (PDirective i)

1263 | what /= EDefns = i

@@ -1279,7 +1279,7 @@ checkInferred fc inf user =

1279 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++

1280 showImp True user

1281 logLvl 10 $ "Checking match"

1282− i <- get

1282+ i <- getIState

1283 tclift $ case matchClause' True i user inf of

1284 Right vs -> return ()

1285 Left (x, y) -> tfail $ At fc

@@ -1293,7 +1293,7 @@ checkInferred fc inf user =

1293

1294inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

1295inferredDiff fc inf user =

1296− do i <- get

1296+ do i <- getIState

1297 logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

1298 showImp True user

1299 tclift $ case matchClause' True i user inf of

src/Idris/Error.hs+3−3

@@ -20,7 +20,7 @@ import Data.Typeable

20iucheck :: Idris ()

21iucheck = do tit <- typeInType

22 when (not tit) $

23− do ist <- get

23+ do ist <- getIState

24 idrisCatch (tclift $ ucheck (idris_constraints ist))

25 (\e -> do let msg = show e

26 setErrLine (getErrLine msg)

@@ -46,13 +46,13 @@ ifail :: String -> Idris ()

46ifail str = throwIO (IErr str)

48ierror :: Err -> Idris ()

49−ierror err = do i <- get

49+ierror err = do i <- getIState

50 throwIO (IErr $ pshow i err)

52tclift :: TC a -> Idris a

53tclift tc = case tc of

54 OK v -> return v

55− Error err -> do i <- get

55+ Error err -> do i <- getIState

56 case err of

57 At (FC f l) e -> setErrLine l

58 _ -> return ()

src/Idris/Parser.hs+6−6

@@ -110,7 +110,7 @@ loadSource lidr f

110 v <- verbose

111 when v $ iputStrLn $ "Type checking " ++ f

112 elabDecls toplevel ds

113− i <- get

113+ i <- getIState

114 -- simplify every definition do give the totality checker

115 -- a better chance

116 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

@@ -118,7 +118,7 @@ loadSource lidr f

118 (map snd (idris_totcheck i))

119 -- build size change graph from simplified definitions

120 iLOG "Totality checking"

121− i <- get

121+ i <- getIState

122 mapM_ buildSCG (idris_totcheck i)

123 mapM_ checkDeclTotality (idris_totcheck i)

124 iLOG ("Finished " ++ f)

@@ -162,7 +162,7 @@ parseTac i = runParser (do t <- pTactic defaultSyntax

162

163parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)

164parseImports fname input

165− = do i <- get

165+ = do i <- getIState

166 case runParser (do whiteSpace

167 mname <- pHeader

168 ps <- many pImport

@@ -170,7 +170,7 @@ parseImports fname input

170 pos <- getPosition

171 return ((mname, ps, rest, pos), i)) i fname input of

172 Left err -> fail (show err)

173− Right (x, i) -> do put i

173+ Right (x, i) -> do putIState i

174 return x

175

176pHeader :: IParser [String]

@@ -275,7 +275,7 @@ pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

275parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->

276 Idris [PDecl]

277parseProg syn fname input pos

278− = do i <- get

278+ = do i <- getIState

279 case runParser (do setPosition pos

280 whiteSpace

281 ps <- many (pDecl syn)

@@ -284,7 +284,7 @@ parseProg syn fname input pos

284 return (concat ps, i')) i fname input of

285 Left err -> do iputStrLn (show err)

286 return []

287− Right (x, i) -> do put i

287+ Right (x, i) -> do putIState i

288 return (collect x)

289

290-- Collect PClauses with the same function name

src/Idris/Prover.hs+7−7

@@ -22,7 +22,7 @@ import Util.Pretty

22prover :: Bool -> Name -> Idris ()

23prover lit x =

24 do ctxt <- getContext

25− i <- get

25+ i <- getIState

26 case lookupTy Nothing x ctxt of

27 [t] -> if elem x (idris_metavars i)

28 then prove ctxt lit x t

@@ -39,13 +39,13 @@ showProof lit n ps

40prove :: Context -> Bool -> Name -> Type -> Idris ()

41prove ctxt lit n ty

42− = do let ps = initElaborator n ctxt ty

42+ = do let ps = initElaborator n ctxt ty

43 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)

44 iLOG $ "Adding " ++ show tm

45 iputStrLn $ showProof lit n prf

46− i <- get

46+ i <- getIState

47 let proofs = proof_list i

48− put (i { proof_list = (n, prf) : proofs })

48+ putIState (i { proof_list = (n, prf) : proofs })

49 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

50 logLvl 3 (show tree)

51 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

@@ -58,7 +58,7 @@ prove ctxt lit n ty

58elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

59elabStep st e = do case runStateT e st of

60 OK (a, st') -> return (a, st')

61− Error a -> do i <- get

61+ Error a -> do i <- getIState

62 fail (pshow i a)

64dumpState :: IState -> ProofState -> IO ()

@@ -110,9 +110,9 @@ lifte st e = do (v, _) <- elabStep st e

110

111ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])

112ploop d prompt prf e

113− = do i <- get

113+ = do i <- getIState

114 when d $ liftIO $ dumpState i (proof e)

115− x <- lift $ getInputLine (prompt ++ "> ")

115+ x <- getInputLine (prompt ++ "> ")

116 (cmd, step) <- case x of

117 Nothing -> fail "Abandoned"

118 Just input -> do return (parseTac i input, input)

src/Idris/REPL.hs+48−40

@@ -53,7 +53,7 @@ repl :: IState -> [FilePath] -> Idris ()

53repl orig mods

54 = H.catch

55 (do let prompt = mkPrompt mods

56− x <- lift $ getInputLine (prompt ++ "> ")

56+ x <- getInputLine (prompt ++ "> ")

57 case x of

58 Nothing -> do iputStrLn "Bye bye"

59 return ()

@@ -78,7 +78,7 @@ lit f = case splitExtension f of

79processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

80processInput cmd orig inputs

81− = do i <- get

81+ = do i <- getIState

82 let fn = case inputs of

83 (f:_) -> f

84 _ -> ""

@@ -86,12 +86,12 @@ processInput cmd orig inputs

86 Left err -> do liftIO $ print err

87 return (Just inputs)

88 Right Reload ->

89− do put (orig { idris_options = idris_options i })

89+ do putIState (orig { idris_options = idris_options i })

90 clearErr

91 mods <- mapM loadModule inputs

92 return (Just inputs)

93 Right (Load f) ->

94− do put (orig { idris_options = idris_options i })

94+ do putIState (orig { idris_options = idris_options i })

95 clearErr

96 mod <- loadModule f

97 return (Just [f])

@@ -111,7 +111,7 @@ processInput cmd orig inputs

111

112resolveProof :: Name -> Idris Name

113resolveProof n'

114− = do i <- get

114+ = do i <- getIState

115 ctxt <- getContext

116 n <- case lookupNames Nothing n' ctxt of

117 [x] -> return x

@@ -121,15 +121,15 @@ resolveProof n'

121

122removeProof :: Name -> Idris ()

123removeProof n =

124− do i <- get

124+ do i <- getIState

125 let proofs = proof_list i

126 let ps = filter ((/= n) . fst) proofs

127− put $ i { proof_list = ps }

127+ putIState $ i { proof_list = ps }

128

129edit :: FilePath -> IState -> Idris ()

130edit "" orig = iputStrLn "Nothing to edit"

131edit f orig

132− = do i <- get

132+ = do i <- getIState

133 env <- liftIO $ getEnvironment

134 let editor = getEditor env

135 let line = case errLine i of

@@ -138,7 +138,7 @@ edit f orig

138 let cmd = editor ++ line ++ f

139 liftIO $ system cmd

140 clearErr

141− put (orig { idris_options = idris_options i })

141+ putIState (orig { idris_options = idris_options i })

142 loadModule f

143 iucheck

144 return ()

@@ -149,7 +149,7 @@ edit f orig

149

150proofs :: IState -> Idris ()

151proofs orig

152− = do i <- get

152+ = do i <- getIState

153 let ps = proof_list i

154 case ps of

155 [] -> iputStrLn "No proofs available"

@@ -166,7 +166,7 @@ process fn Help = iputStrLn displayHelp

166process fn (Eval t)

167 = do (tm, ty) <- elabVal toplevel False t

168 ctxt <- getContext

169− ist <- get

169+ ist <- getIState

170 let tm' = normaliseAll ctxt [] tm

171 let ty' = normaliseAll ctxt [] ty

172 logLvl 3 $ "Raw: " ++ show (tm', ty')

@@ -186,7 +186,7 @@ process fn (ExecVal t)

186 where fc = FC "(input)" 0

187process fn (Check (PRef _ n))

188 = do ctxt <- getContext

189− ist <- get

189+ ist <- getIState

190 imp <- impShow

191 case lookupTy Nothing n ctxt of

192 ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++

@@ -194,20 +194,20 @@ process fn (Check (PRef _ n))

194 [] -> iputStrLn $ "No such variable " ++ show n

195process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

196 ctxt <- getContext

197− ist <- get

197+ ist <- getIState

198 imp <- impShow

199 let ty' = normaliseC ctxt [] ty

200 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

201 showImp imp (delab ist ty))

202

203−process fn (DocStr n) = do i <- get

203+process fn (DocStr n) = do i <- getIState

204 case lookupCtxtName Nothing n (idris_docstrings i) of

205 [] -> iputStrLn $ "No documentation for " ++ show n

206 ns -> mapM_ showDoc ns

207 where showDoc (n, d)

208 = do doc <- getDocs n

209 iputStrLn $ show doc

210−process fn Universes = do i <- get

210+process fn Universes = do i <- getIState

211 let cs = idris_constraints i

212-- iputStrLn $ showSep "\n" (map show cs)

213 liftIO $ print (map fst cs)

@@ -216,7 +216,7 @@ process fn Universes = do i <- get

216 case ucheck cs of

217 Error e -> iputStrLn $ pshow i e

218 OK _ -> iputStrLn "Universes OK"

219−process fn (Defn n) = do i <- get

219+process fn (Defn n) = do i <- getIState

220 iputStrLn "Compiled patterns:\n"

221 liftIO $ print (lookupDef Nothing n (tt_ctxt i))

222 case lookupCtxt Nothing n (idris_patdefs i) of

@@ -230,12 +230,12 @@ process fn (Defn n) = do i <- get

230 = do liftIO $ putStr $ showImp True (delab i lhs)

231 liftIO $ putStr " = "

232 liftIO $ putStrLn $ showImp True (delab i rhs)

233−process fn (TotCheck n) = do i <- get

233+process fn (TotCheck n) = do i <- getIState

234 case lookupTotal n (tt_ctxt i) of

235 [t] -> iputStrLn (showTotal t i)

236 _ -> return ()

237process fn (DebugInfo n)

238− = do i <- get

238+ = do i <- getIState

239 let oi = lookupCtxtName Nothing n (idris_optimisation i)

240 when (not (null oi)) $ iputStrLn (show oi)

241 let si = lookupCtxt Nothing n (idris_statics i)

@@ -247,25 +247,25 @@ process fn (DebugInfo n)

247 do print (head d)

248 let cg = lookupCtxtName Nothing n (idris_callgraph i)

249 findUnusedArgs (map fst cg)

250− i <- get

250+ i <- getIState

251 let cg' = lookupCtxtName Nothing n (idris_callgraph i)

252 sc <- checkSizeChange n

253 iputStrLn $ "Size change: " ++ show sc

254 when (not (null cg')) $ do iputStrLn "Call graph:\n"

255 iputStrLn (show cg')

256−process fn (Info n) = do i <- get

256+process fn (Info n) = do i <- getIState

257 case lookupCtxt Nothing n (idris_classes i) of

258 [c] -> classInfo c

259 _ -> iputStrLn "Not a class"

260process fn (Search t) = iputStrLn "Not implemented"

261process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

262 ctxt <- getContext

263− ist <- get

263+ ist <- getIState

264 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm

265 iputStrLn (show (delab ist tm'))

266

267process fn (RmProof n')

268− = do i <- get

268+ = do i <- getIState

269 n <- resolveProof n'

270 let proofs = proof_list i

271 case lookup n proofs of

@@ -276,15 +276,15 @@ process fn (RmProof n')

276 where

277 insertMetavar :: Name -> Idris ()

278 insertMetavar n =

279− do i <- get

279+ do i <- getIState

280 let ms = idris_metavars i

281− put $ i { idris_metavars = n : ms }

281+ putIState $ i { idris_metavars = n : ms }

282

283process fn (AddProof prf)

284 = do let fb = fn ++ "~"

285 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!

286 prog <- liftIO $ readFile fb

287− i <- get

287+ i <- getIState

288 let proofs = proof_list i

289 n' <- case prf of

290 Nothing -> case proofs of

@@ -301,7 +301,7 @@ process fn (AddProof prf)

301 where ls = (lines prog)

302

303process fn (ShowProof n')

304− = do i <- get

304+ = do i <- getIState

305 n <- resolveProof n'

306 let proofs = proof_list i

307 case lookup n proofs of

@@ -310,26 +310,26 @@ process fn (ShowProof n')

310

311process fn (Prove n')

312 = do ctxt <- getContext

313− ist <- get

313+ ist <- getIState

314 n <- case lookupNames Nothing n' ctxt of

315 [x] -> return x

316 [] -> return n'

317 ns -> fail $ pshow ist (CantResolveAlts (map show ns))

318 prover (lit fn) n

319 -- recheck totality

320− i <- get

320+ i <- getIState

321 totcheck (FC "(input)" 0, n)

322 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

323 mapM_ checkDeclTotality (idris_totcheck i)

324

325process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

326 ctxt <- getContext

327− ist <- get

327+ ist <- getIState

328 let tm' = hnf ctxt [] tm

329 iputStrLn (show (delab ist tm'))

330−process fn TTShell = do ist <- get

330+process fn TTShell = do ist <- getIState

331 let shst = initState (tt_ctxt ist)

332− shst' <- lift $ runShell shst

332+ runShell shst

333 return ()

334process fn Execute = do (m, _) <- elabVal toplevel False

335 (PApp fc

@@ -361,7 +361,7 @@ process fn (Pattelab t)

361 = do (tm, ty) <- elabVal toplevel True t

362 iputStrLn $ show tm ++ "\n\n : " ++ show ty

363

364−process fn (Missing n) = do i <- get

364+process fn (Missing n) = do i <- getIState

365 case lookupDef Nothing n (tt_ctxt i) of

366 [CaseOp _ _ _ _ _ args t _ _]

367 -> do tms <- genMissing n args t

@@ -369,7 +369,7 @@ process fn (Missing n) = do i <- get

369 [] -> iputStrLn $ show n ++ " undefined"

370 _ -> iputStrLn $ "Ambiguous name"

371process fn Metavars

372− = do ist <- get

372+ = do ist <- getIState

373 let mvs = idris_metavars ist \\ primDefs

374 case mvs of

375 [] -> iputStrLn "No global metavariables to solve"

@@ -396,7 +396,7 @@ dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

396dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

397

398dumpInstance :: Name -> Idris ()

399−dumpInstance n = do i <- get

399+dumpInstance n = do i <- getIState

400 ctxt <- getContext

401 imp <- impShow

402 case lookupTy Nothing n ctxt of

@@ -489,12 +489,20 @@ help =

489 ([":q",":quit"], "", "Exit the Idris system")

490 ]

491

492+idrisCompletion :: CompletionFunc (StateT IState IO)

493+idrisCompletion (before, after) = return (before, [])

494+

495+haskelineSettings :: Settings (StateT IState IO)

496+haskelineSettings = setComplete idrisCompletion defaultSettings

497+

492-- invoke as if from command line

498-- invoke as if from command line

493idris :: [Opt] -> IO IState

499idris :: [Opt] -> IO IState

500+idris opts = execStateT (runInputT haskelineSettings $ idrisMain opts) idrisInit

501+

494−idris opts = runInputT defaultSettings $ execStateT (idrisMain opts) idrisInit

502+--runInputT haskelineSettings $ execStateT (idrisMain opts) idrisInit

495

503

496idrisMain :: [Opt] -> Idris ()

504idrisMain :: [Opt] -> Idris ()

497−idrisMain opts =

505+idrisMain opts =

498 do let inputs = opt getFile opts

506 do let inputs = opt getFile opts

499 let runrepl = not (NoREPL `elem` opts)

507 let runrepl = not (NoREPL `elem` opts)

500 let output = opt getOutput opts

508 let output = opt getOutput opts

@@ -510,8 +518,8 @@ idrisMain opts =

510 let tgt = case opt getTarget opts of

518 let tgt = case opt getTarget opts of

511 [] -> ViaC

519 [] -> ViaC

512 xs -> last xs

520 xs -> last xs

513− when (DefaultTotal `elem` opts) $ do i <- get

521+ when (DefaultTotal `elem` opts) $ do i <- getIState

514− put (i { default_total = True })

522+ putIState (i { default_total = True })

515 setREPL runrepl

523 setREPL runrepl

516 setVerbose runrepl

524 setVerbose runrepl

517 setCmdLine opts

525 setCmdLine opts

@@ -536,8 +544,8 @@ idrisMain opts =

536 elabPrims

544 elabPrims

537 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

545 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

538 return ()

546 return ()

539− when runrepl $ iputStrLn banner

547+ when runrepl $ iputStrLn banner

540− ist <- get

548+ ist <- getIState

541 mods <- mapM loadModule inputs

549 mods <- mapM loadModule inputs

542 ok <- noErrors

550 ok <- noErrors

543 when ok $ case output of

551 when ok $ case output of

src/Idris/UnusedArgs.hs+2−2

@@ -14,7 +14,7 @@ findUnusedArgs ns = mapM_ traceUnused ns

15traceUnused :: Name -> Idris ()

16traceUnused n

17− = do i <- get

17+ = do i <- getIState

18 case lookupCtxt Nothing n (idris_callgraph i) of

19 [CGInfo args calls scg usedns _] ->

20 do let argpos = zip args [0..]

@@ -38,7 +38,7 @@ used path g j

38 | (g, j) `elem` path = return False -- cycle, never used on the way

39 | otherwise

40 = do logLvl 5 $ (show ((g, j) : path))

41− i <- get

41+ i <- getIState

42 case lookupCtxt Nothing g (idris_callgraph i) of

43 [CGInfo args calls scg usedns unused] ->

44 if (j >= length args)

src/Main.hs+1−1

@@ -39,7 +39,7 @@ import Paths_idris

40main = do xs <- getArgs

41 let opts = parseArgs xs

42− runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

42+ execStateT (runInputT haskelineSettings $ runIdris opts) idrisInit

44runIdris :: [Opt] -> Idris ()

45runIdris opts = do