f31c76a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:edwinb/Idris-dev

f31c76aEdwin Brady14 years ago

src/Core/ProofShell.hs+21−17

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,21 +57,23 @@ 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

61+runShell st = runInputT defaultSettings $ runShell' st

62+ where

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

63+ runShell' st = do (prompt, parser) <-

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

64+ maybe (return ("TT# ", parseCommand))

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

65+ (\st -> do outputStrLn . render . pretty $ st

62− return (show (thname st) ++ "# ", parseTactic))

66+ return (show (thname st) ++ "# ", parseTactic))

63− (prf st)

67+ (prf st)

64− x <- getInputLine prompt

68+ x <- getInputLine prompt

65− cmd <- case x of

69+ cmd <- case x of

66− Nothing -> return $ Right Quit

70+ Nothing -> return $ Right Quit

67− Just input -> return (parser input)

71+ Just input -> return (parser input)

68− case cmd of

72+ case cmd of

69− Left err -> do outputStrLn (show err)

73+ Left err -> do outputStrLn (show err)

70− runShell st

74+ runShell' st

71− Right cmd -> do let (st', r) = processCommand cmd st

75+ Right cmd -> do let (st', r) = processCommand cmd st

72− outputStrLn r

76+ outputStrLn r

73− if (not (exitNow st')) then runShell st'

77+ if (not (exitNow st')) then runShell' st'

74− else return st'

78+ else return 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+92−92

@@ -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,45 +107,45 @@ 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

151getIState = get

@@ -154,9 +154,9 @@ putIState :: IState -> Idris ()

154putIState = 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 = StateT IState IO

140

141-- Commands in the REPL

142

src/Idris/Completion.hsnew file+143

@@ -0,0 +1,143 @@

1+module Idris.Completion (replCompletion, proverCompletion) where

3+import Core.Evaluate (ctxtAlist)

4+import Core.TT

6+import Idris.AbsSyntaxTree

8+import Control.Monad.State.Strict

10+import Data.List

11+import Data.Maybe

12+

13+import System.Console.Haskeline

14+

15+-- TODO: add specific classes of identifiers to complete, fx metavariables

16+-- | A specification of the arguments that REPL commands can take

17+data CmdArg = ExprArg -- ^ The command takes an expression

18+ | NameArg -- ^ The command takes a name

19+ | FileArg -- ^ The command takes a file

20+ | ModuleArg -- ^ The command takes a module name

21+ | OptionArg -- ^ The command takes an option

22+

23+-- | Information about how to complete the various commands

24+cmdArgs :: [(String, CmdArg)]

25+cmdArgs = [ (":t", ExprArg)

26+ , (":miss", NameArg)

27+ , (":missing", NameArg)

28+ , (":i", NameArg)

29+ , (":info", NameArg)

30+ , (":total", NameArg)

31+ , (":l", FileArg)

32+ , (":load", FileArg)

33+ , (":m", ModuleArg) -- NOTE: Argumentless form is a different command

34+ , (":p", NameArg)

35+ , (":prove", NameArg)

36+ , (":a", NameArg)

37+ , (":addproof", NameArg)

38+ , (":rmproof", NameArg)

39+ , (":showproof", NameArg)

40+ , (":c", FileArg)

41+ , (":compile", FileArg)

42+ , (":js", FileArg)

43+ , (":javascript", FileArg)

44+ , (":set", OptionArg)

45+ , (":unset", OptionArg)

46+ ]

47+commands = map fst cmdArgs

48+

49+-- | A specification of the arguments that tactics can take

50+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

51+ | ExprTArg

52+ | AltsTArg

53+

54+-- | A list of available tactics and their argument requirements

55+tacticArgs :: [(String, Maybe TacticArg)]

56+tacticArgs = [ ("intro", Nothing)

57+ , ("intros", Nothing)

58+ , ("refine", Just ExprTArg)

59+ , ("rewrite", Just ExprTArg)

60+ , ("let", Nothing) -- FIXME syntax for let

61+ , ("focus", Just ExprTArg)

62+ , ("exact", Just ExprTArg)

63+ , ("reflect", Just ExprTArg)

64+ , ("try", Just AltsTArg)

65+ ] ++ map (\x -> (x, Nothing)) [

66+ "intro", "intros", "compute", "trivial", "solve", "attack",

67+ "state", "term", "undo", "qed", "abandon", ":q"

68+ ]

69+tactics = map fst tacticArgs

70+

71+-- | Convert a name into a string usable for completion. Filters out names

72+-- that users probably don't want to see.

73+nameString :: Name -> Maybe String

74+nameString (UN ('@':_)) = Nothing

75+nameString (UN ('#':_)) = Nothing

76+nameString (UN n) = Just n

77+nameString (NS n _) = nameString n

78+nameString _ = Nothing

79+

80+-- FIXME: Respect module imports

81+-- | Get the user-visible names from the current interpreter state.

82+names :: Idris[String]

83+names = do i <- get

84+ let ctxt = tt_ctxt i

85+ return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt

86+

87+

88+modules :: Idris [String]

89+modules = do i <- get

90+ return $ map show $ imported i

91+

92+

93+

94+completeWith :: [String] -> String -> [Completion]

95+completeWith ns n = if uniqueExists

96+ then [simpleCompletion n]

97+ else map simpleCompletion prefixMatches

98+ where prefixMatches = filter (isPrefixOf n) ns

99+ uniqueExists = n `elem` prefixMatches

100+

101+completeName :: [String] -> String -> Idris [Completion]

102+completeName extra n = do ns <- names

103+ return $ completeWith (extra ++ ns) n

104+

105+completeExpr :: [String] -> CompletionFunc Idris

106+completeExpr extra = completeWord Nothing " \t" (completeName extra)

107+

108+completeOption :: CompletionFunc Idris

109+completeOption = completeWord Nothing " \t" completeOpt

110+ where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])

111+

112+isWhitespace :: Char -> Bool

113+isWhitespace = (flip elem) " \t\n"

114+

115+-- | Get the completion function for a particular command

116+completeCmd :: String -> CompletionFunc Idris

117+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs

118+ where completeArg FileArg = completeFilename (prev, next)

119+ completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

120+ completeArg OptionArg = completeOption (prev, next)

121+ completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

122+ completeArg ExprArg = completeExpr [] (prev, next)

123+ completeCmdName = return $ ("", completeWith commands cmd)

124+

125+replCompletion :: CompletionFunc Idris

126+replCompletion (prev, next) = case firstWord of

127+ ':':cmdName -> completeCmd (':':cmdName) (prev, next)

128+ _ -> completeExpr [] (prev, next)

129+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev

130+

131+

132+completeTactic :: [String] -> String -> CompletionFunc Idris

133+completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs

134+ where completeTacName = return $ ("", completeWith tactics tac)

135+ completeArg Nothing = noCompletion (prev, next)

136+ completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!

137+ completeArg (Just ExprTArg) = completeExpr as (prev, next)

138+ completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO

139+

140+

141+proverCompletion :: [String] -> CompletionFunc Idris

142+proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)

143+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev

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 5 ("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+12−11

@@ -63,12 +63,13 @@ fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\

63loadModule :: FilePath -> Idris String

64loadModule f

65 = idrisCatch (do i <- getIState

66+ let file = takeWhile (/= ' ') f

66 ibcsd <- valIBCSubDir i

67 ibcsd <- valIBCSubDir i

67 ids <- allImportDirs i

68 ids <- allImportDirs i

68− fp <- liftIO $ findImport ids ibcsd f

69+ fp <- liftIO $ findImport ids ibcsd file

69− if f `elem` imported i

70+ if file `elem` imported i

70− then iLOG $ "Already read " ++ f

71+ then iLOG $ "Already read " ++ file

71− else do putIState (i { imported = f : imported i })

72+ else do putIState (i { imported = file : imported i })

72 case fp of

73 case fp of

73 IDR fn -> loadSource False fn

74 IDR fn -> loadSource False fn

74 LIDR fn -> loadSource True fn

75 LIDR fn -> loadSource True fn

@@ -78,7 +79,7 @@ loadModule f

78 case src of

79 case src of

79 IDR sfn -> loadSource False sfn

80 IDR sfn -> loadSource False sfn

80 LIDR sfn -> loadSource True sfn)

81 LIDR sfn -> loadSource True sfn)

81− let (dir, fh) = splitFileName f

82+ let (dir, fh) = splitFileName file

82 return (dropExtension fh))

83 return (dropExtension fh))

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

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

84 setErrLine (getErrLine msg)

85 setErrLine (getErrLine msg)

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

110 v <- verbose

111 v <- verbose

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

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

112 elabDecls toplevel ds

113 elabDecls toplevel ds

113− i <- get

114+ i <- getIState

114 -- simplify every definition do give the totality checker

115 -- simplify every definition do give the totality checker

115 -- a better chance

116 -- a better chance

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

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

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

118 (map snd (idris_totcheck i))

119 (map snd (idris_totcheck i))

119 -- build size change graph from simplified definitions

120 -- build size change graph from simplified definitions

120 iLOG "Totality checking"

121 iLOG "Totality checking"

121− i <- get

122+ i <- getIState

122 mapM_ buildSCG (idris_totcheck i)

123 mapM_ buildSCG (idris_totcheck i)

123 mapM_ checkDeclTotality (idris_totcheck i)

124 mapM_ checkDeclTotality (idris_totcheck i)

124 iLOG ("Finished " ++ f)

125 iLOG ("Finished " ++ f)

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

162

163

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

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

164parseImports fname input

165parseImports fname input

165− = do i <- get

166+ = do i <- getIState

166 case runParser (do whiteSpace

167 case runParser (do whiteSpace

167 mname <- pHeader

168 mname <- pHeader

168 ps <- many pImport

169 ps <- many pImport

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

170 pos <- getPosition

171 pos <- getPosition

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

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

172 Left err -> fail (show err)

173 Left err -> fail (show err)

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

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

174 return x

175 return x

175

176

176pHeader :: IParser [String]

177pHeader :: IParser [String]

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

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

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

276 Idris [PDecl]

277 Idris [PDecl]

277parseProg syn fname input pos

278parseProg syn fname input pos

278− = do i <- get

279+ = do i <- getIState

279 case runParser (do setPosition pos

280 case runParser (do setPosition pos

280 whiteSpace

281 whiteSpace

281 ps <- many (pDecl syn)

282 ps <- many (pDecl syn)

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

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

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

285 Left err -> do iputStrLn (show err)

286 Left err -> do iputStrLn (show err)

286 return []

287 return []

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

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

288 return (collect x)

289 return (collect x)

289

290

290-- Collect PClauses with the same function name

291-- Collect PClauses with the same function name

src/Idris/Prover.hs+30−13

@@ -13,8 +13,10 @@ import Idris.ElabTerm

13import Idris.Parser

14import Idris.Error

15import Idris.DataOpts

16+import Idris.Completion

17import System.Console.Haskeline

18import System.Console.Haskeline

19+import System.Console.Haskeline.History

18import Control.Monad.State

20import Control.Monad.State

20import Util.Pretty

22import Util.Pretty

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

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

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

23prover lit x =

25prover lit x =

24 do ctxt <- getContext

26 do ctxt <- getContext

25− i <- get

27+ i <- getIState

26 case lookupTy Nothing x ctxt of

28 case lookupTy Nothing x ctxt of

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

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

28 then prove ctxt lit x t

30 then prove ctxt lit x t

@@ -37,15 +39,23 @@ showProof lit n ps

37 where bird = if lit then "> " else ""

39 where bird = if lit then "> " else ""

38 break = "\n" ++ bird

40 break = "\n" ++ bird

42+proverSettings :: ElabState [PDecl] -> Settings Idris

43+proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings

44+ where assumptionNames = case envAtFocus (proof e) of

45+ OK env -> names env

46+ names [] = []

47+ names ((MN _ _, _) : bs) = names bs

48+ names ((n, _) : bs) = show n : names bs

49+

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

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

41prove ctxt lit n ty

51prove ctxt lit n ty

42− = do let ps = initElaborator n ctxt ty

52+ = do let ps = initElaborator n ctxt ty

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

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

44 iLOG $ "Adding " ++ show tm

54 iLOG $ "Adding " ++ show tm

45 iputStrLn $ showProof lit n prf

55 iputStrLn $ showProof lit n prf

46− i <- get

56+ i <- getIState

47 let proofs = proof_list i

57 let proofs = proof_list i

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

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

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

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

50 logLvl 3 (show tree)

60 logLvl 3 (show tree)

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

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

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

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

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

59elabStep st e = do case runStateT e st of

69elabStep st e = do case runStateT e st of

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

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

61− Error a -> do i <- get

71+ Error a -> do i <- getIState

62 fail (pshow i a)

72 fail (pshow i a)

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

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

@@ -108,18 +118,25 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a

108lifte st e = do (v, _) <- elabStep st e

118lifte st e = do (v, _) <- elabStep st e

109 return v

119 return v

110

120

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

121+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

112−ploop d prompt prf e

122+ploop d prompt prf e h

113− = do i <- get

123+ = do i <- getIState

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

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

125+ (x, h') <- runInputT (proverSettings e) $

126+ -- Manually track the history so that we can use the proof state

127+ do _ <- case h of

128+ Just history -> putHistory history

129+ Nothing -> return ()

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

130+ l <- getInputLine (prompt ++ "> ")

131+ h' <- getHistory

132+ return (l, Just h')

116 (cmd, step) <- case x of

133 (cmd, step) <- case x of

117 Nothing -> fail "Abandoned"

134 Nothing -> fail "Abandoned"

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

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

119 case cmd of

136 case cmd of

120 Right Abandon -> fail "Abandoned"

137 Right Abandon -> fail "Abandoned"

121 _ -> return ()

138 _ -> return ()

122− (d, st, done, prf') <- idrisCatch

139+ (d, st, done, prf') <- idrisCatch

123 (case cmd of

140 (case cmd of

124 Left err -> do iputStrLn (show err)

141 Left err -> do iputStrLn (show err)

125 return (False, e, False, prf)

142 return (False, e, False, prf)

@@ -140,7 +157,7 @@ ploop d prompt prf e

140 return (True, st, False, prf ++ [step]))

157 return (True, st, False, prf ++ [step]))

141 (\err -> do iputStrLn (show err)

158 (\err -> do iputStrLn (show err)

142 return (False, e, False, prf))

159 return (False, e, False, prf))

143− if done then do (tm, _) <- elabStep st get_term

160+ if done then do (tm, _) <- elabStep st get_term

144 return (tm, prf')

161 return (tm, prf')

145− else ploop d prompt prf' st

162+ else ploop d prompt prf' st h'

146

163

src/Idris/REPL.hs+51−46

@@ -16,6 +16,7 @@ import Idris.Primitives

16import Idris.Coverage

17import Idris.UnusedArgs

18import Idris.Docs

19+import Idris.Completion

20import Paths_idris

21import Paths_idris

21import Util.System

22import Util.System

@@ -49,23 +50,23 @@ import Data.List

49import Data.Char

50import Data.Char

50import Data.Version

51import Data.Version

52−repl :: IState -> [FilePath] -> Idris ()

53+repl :: IState -> [FilePath] -> InputT Idris ()

53repl orig mods

54repl orig mods

54 = H.catch

55 = H.catch

55 (do let prompt = mkPrompt mods

56 (do let prompt = mkPrompt mods

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

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

57 case x of

58 case x of

58− Nothing -> do iputStrLn "Bye bye"

59+ Nothing -> do lift $ iputStrLn "Bye bye"

59 return ()

60 return ()

60 Just input -> H.catch

61 Just input -> H.catch

61− (do ms <- processInput input orig mods

62+ (do ms <- lift $ processInput input orig mods

62 case ms of

63 case ms of

63 Just mods -> repl orig mods

64 Just mods -> repl orig mods

64 Nothing -> return ())

65 Nothing -> return ())

65 ctrlC)

66 ctrlC)

66 ctrlC

67 ctrlC

67− where ctrlC :: SomeException -> Idris ()

68+ where ctrlC :: SomeException -> InputT Idris ()

68− ctrlC e = do iputStrLn (show e)

69+ ctrlC e = do lift $ iputStrLn (show e)

69 repl orig mods

70 repl orig mods

71mkPrompt [] = "Idris"

72mkPrompt [] = "Idris"

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

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

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

80processInput cmd orig inputs

81processInput cmd orig inputs

81− = do i <- get

82+ = do i <- getIState

82 let fn = case inputs of

83 let fn = case inputs of

83 (f:_) -> f

84 (f:_) -> f

84 _ -> ""

85 _ -> ""

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

86 Left err -> do liftIO $ print err

87 Left err -> do liftIO $ print err

87 return (Just inputs)

88 return (Just inputs)

88 Right Reload ->

89 Right Reload ->

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

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

90 clearErr

91 clearErr

91 mods <- mapM loadModule inputs

92 mods <- mapM loadModule inputs

92 return (Just inputs)

93 return (Just inputs)

93 Right (Load f) ->

94 Right (Load f) ->

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

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

95 clearErr

96 clearErr

96 mod <- loadModule f

97 mod <- loadModule f

97 return (Just [f])

98 return (Just [f])

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

111

112

112resolveProof :: Name -> Idris Name

113resolveProof :: Name -> Idris Name

113resolveProof n'

114resolveProof n'

114− = do i <- get

115+ = do i <- getIState

115 ctxt <- getContext

116 ctxt <- getContext

116 n <- case lookupNames Nothing n' ctxt of

117 n <- case lookupNames Nothing n' ctxt of

117 [x] -> return x

118 [x] -> return x

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

121

122

122removeProof :: Name -> Idris ()

123removeProof :: Name -> Idris ()

123removeProof n =

124removeProof n =

124− do i <- get

125+ do i <- getIState

125 let proofs = proof_list i

126 let proofs = proof_list i

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

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

127− put $ i { proof_list = ps }

128+ putIState $ i { proof_list = ps }

128

129

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

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

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

131edit "" orig = iputStrLn "Nothing to edit"

131edit f orig

132edit f orig

132− = do i <- get

133+ = do i <- getIState

133 env <- liftIO $ getEnvironment

134 env <- liftIO $ getEnvironment

134 let editor = getEditor env

135 let editor = getEditor env

135 let line = case errLine i of

136 let line = case errLine i of

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

138 let cmd = editor ++ line ++ f

139 let cmd = editor ++ line ++ f

139 liftIO $ system cmd

140 liftIO $ system cmd

140 clearErr

141 clearErr

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

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

142 loadModule f

143 loadModule f

143 iucheck

144 iucheck

144 return ()

145 return ()

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

149

150

150proofs :: IState -> Idris ()

151proofs :: IState -> Idris ()

151proofs orig

152proofs orig

152− = do i <- get

153+ = do i <- getIState

153 let ps = proof_list i

154 let ps = proof_list i

154 case ps of

155 case ps of

155 [] -> iputStrLn "No proofs available"

156 [] -> iputStrLn "No proofs available"

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

166process fn (Eval t)

167process fn (Eval t)

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

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

168 ctxt <- getContext

169 ctxt <- getContext

169− ist <- get

170+ ist <- getIState

170 let tm' = normaliseAll ctxt [] tm

171 let tm' = normaliseAll ctxt [] tm

171 let ty' = normaliseAll ctxt [] ty

172 let ty' = normaliseAll ctxt [] ty

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

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

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

186 where fc = FC "(input)" 0

187 where fc = FC "(input)" 0

187process fn (Check (PRef _ n))

188process fn (Check (PRef _ n))

188 = do ctxt <- getContext

189 = do ctxt <- getContext

189− ist <- get

190+ ist <- getIState

190 imp <- impShow

191 imp <- impShow

191 case lookupTy Nothing n ctxt of

192 case lookupTy Nothing n ctxt of

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

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

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

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

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

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

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

196 ctxt <- getContext

197 ctxt <- getContext

197− ist <- get

198+ ist <- getIState

198 imp <- impShow

199 imp <- impShow

199 let ty' = normaliseC ctxt [] ty

200 let ty' = normaliseC ctxt [] ty

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

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

201 showImp imp (delab ist ty))

202 showImp imp (delab ist ty))

202

203

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

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

204 case lookupCtxtName Nothing n (idris_docstrings i) of

205 case lookupCtxtName Nothing n (idris_docstrings i) of

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

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

206 ns -> mapM_ showDoc ns

207 ns -> mapM_ showDoc ns

207 where showDoc (n, d)

208 where showDoc (n, d)

208 = do doc <- getDocs n

209 = do doc <- getDocs n

209 iputStrLn $ show doc

210 iputStrLn $ show doc

210−process fn Universes = do i <- get

211+process fn Universes = do i <- getIState

211 let cs = idris_constraints i

212 let cs = idris_constraints i

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

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

213 liftIO $ print (map fst cs)

214 liftIO $ print (map fst cs)

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

216 case ucheck cs of

217 case ucheck cs of

217 Error e -> iputStrLn $ pshow i e

218 Error e -> iputStrLn $ pshow i e

218 OK _ -> iputStrLn "Universes OK"

219 OK _ -> iputStrLn "Universes OK"

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

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

220 iputStrLn "Compiled patterns:\n"

221 iputStrLn "Compiled patterns:\n"

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

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

222 case lookupCtxt Nothing n (idris_patdefs i) of

223 case lookupCtxt Nothing n (idris_patdefs i) of

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

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

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

231 liftIO $ putStr " = "

232 liftIO $ putStr " = "

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

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

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

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

234 case lookupTotal n (tt_ctxt i) of

235 case lookupTotal n (tt_ctxt i) of

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

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

236 _ -> return ()

237 _ -> return ()

237process fn (DebugInfo n)

238process fn (DebugInfo n)

238− = do i <- get

239+ = do i <- getIState

239 let oi = lookupCtxtName Nothing n (idris_optimisation i)

240 let oi = lookupCtxtName Nothing n (idris_optimisation i)

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

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

241 let si = lookupCtxt Nothing n (idris_statics i)

242 let si = lookupCtxt Nothing n (idris_statics i)

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

247 do print (head d)

248 do print (head d)

248 let cg = lookupCtxtName Nothing n (idris_callgraph i)

249 let cg = lookupCtxtName Nothing n (idris_callgraph i)

249 findUnusedArgs (map fst cg)

250 findUnusedArgs (map fst cg)

250− i <- get

251+ i <- getIState

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

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

252 sc <- checkSizeChange n

253 sc <- checkSizeChange n

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

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

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

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

255 iputStrLn (show cg')

256 iputStrLn (show cg')

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

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

257 case lookupCtxt Nothing n (idris_classes i) of

258 case lookupCtxt Nothing n (idris_classes i) of

258 [c] -> classInfo c

259 [c] -> classInfo c

259 _ -> iputStrLn "Not a class"

260 _ -> iputStrLn "Not a class"

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

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

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

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

262 ctxt <- getContext

263 ctxt <- getContext

263− ist <- get

264+ ist <- getIState

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

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

265 iputStrLn (show (delab ist tm'))

266 iputStrLn (show (delab ist tm'))

266

267

267process fn (RmProof n')

268process fn (RmProof n')

268− = do i <- get

269+ = do i <- getIState

269 n <- resolveProof n'

270 n <- resolveProof n'

270 let proofs = proof_list i

271 let proofs = proof_list i

271 case lookup n proofs of

272 case lookup n proofs of

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

276 where

277 where

277 insertMetavar :: Name -> Idris ()

278 insertMetavar :: Name -> Idris ()

278 insertMetavar n =

279 insertMetavar n =

279− do i <- get

280+ do i <- getIState

280 let ms = idris_metavars i

281 let ms = idris_metavars i

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

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

282

283

283process fn (AddProof prf)

284process fn (AddProof prf)

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

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

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

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

286 prog <- liftIO $ readFile fb

287 prog <- liftIO $ readFile fb

287− i <- get

288+ i <- getIState

288 let proofs = proof_list i

289 let proofs = proof_list i

289 n' <- case prf of

290 n' <- case prf of

290 Nothing -> case proofs of

291 Nothing -> case proofs of

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

301 where ls = (lines prog)

302 where ls = (lines prog)

302

303

303process fn (ShowProof n')

304process fn (ShowProof n')

304− = do i <- get

305+ = do i <- getIState

305 n <- resolveProof n'

306 n <- resolveProof n'

306 let proofs = proof_list i

307 let proofs = proof_list i

307 case lookup n proofs of

308 case lookup n proofs of

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

310

311

311process fn (Prove n')

312process fn (Prove n')

312 = do ctxt <- getContext

313 = do ctxt <- getContext

313− ist <- get

314+ ist <- getIState

314 n <- case lookupNames Nothing n' ctxt of

315 n <- case lookupNames Nothing n' ctxt of

315 [x] -> return x

316 [x] -> return x

316 [] -> return n'

317 [] -> return n'

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

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

318 prover (lit fn) n

319 prover (lit fn) n

319 -- recheck totality

320 -- recheck totality

320− i <- get

321+ i <- getIState

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

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

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

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

323 mapM_ checkDeclTotality (idris_totcheck i)

324 mapM_ checkDeclTotality (idris_totcheck i)

324

325

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

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

326 ctxt <- getContext

327 ctxt <- getContext

327− ist <- get

328+ ist <- getIState

328 let tm' = hnf ctxt [] tm

329 let tm' = hnf ctxt [] tm

329 iputStrLn (show (delab ist tm'))

330 iputStrLn (show (delab ist tm'))

330−process fn TTShell = do ist <- get

331+process fn TTShell = do ist <- getIState

331 let shst = initState (tt_ctxt ist)

332 let shst = initState (tt_ctxt ist)

332− shst' <- lift $ runShell shst

333+ runShell shst

333 return ()

334 return ()

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

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

335 (PApp fc

336 (PApp fc

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

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

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

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

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

363

364

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

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

365 case lookupDef Nothing n (tt_ctxt i) of

366 case lookupDef Nothing n (tt_ctxt i) of

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

367 [CaseOp _ _ _ _ _ args t _ _]

367 -> do tms <- genMissing n args t

368 -> do tms <- genMissing n args t

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

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

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

370 _ -> iputStrLn $ "Ambiguous name"

371 _ -> iputStrLn $ "Ambiguous name"

371process fn Metavars

372process fn Metavars

372− = do ist <- get

373+ = do ist <- getIState

373 let mvs = idris_metavars ist \\ primDefs

374 let mvs = idris_metavars ist \\ primDefs

374 case mvs of

375 case mvs of

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

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

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

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

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

397

398

398dumpInstance :: Name -> Idris ()

399dumpInstance :: Name -> Idris ()

399−dumpInstance n = do i <- get

400+dumpInstance n = do i <- getIState

400 ctxt <- getContext

401 ctxt <- getContext

401 imp <- impShow

402 imp <- impShow

402 case lookupTy Nothing n ctxt of

403 case lookupTy Nothing n ctxt of

@@ -489,12 +490,16 @@ help =

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

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

490 ]

491 ]

491

492

493+

494+replSettings :: Settings Idris

495+replSettings = setComplete replCompletion defaultSettings

496+

492-- invoke as if from command line

497-- invoke as if from command line

493idris :: [Opt] -> IO IState

498idris :: [Opt] -> IO IState

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

499+idris opts = execStateT (idrisMain opts) idrisInit

495

500

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

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

497−idrisMain opts =

502+idrisMain opts =

498 do let inputs = opt getFile opts

503 do let inputs = opt getFile opts

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

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

500 let output = opt getOutput opts

505 let output = opt getOutput opts

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

510 let tgt = case opt getTarget opts of

515 let tgt = case opt getTarget opts of

511 [] -> ViaC

516 [] -> ViaC

512 xs -> last xs

517 xs -> last xs

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

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

514− put (i { default_total = True })

519+ putIState (i { default_total = True })

515 setREPL runrepl

520 setREPL runrepl

516 setVerbose runrepl

521 setVerbose runrepl

517 setCmdLine opts

522 setCmdLine opts

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

536 elabPrims

541 elabPrims

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

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

538 return ()

543 return ()

539− when runrepl $ iputStrLn banner

544+ when runrepl $ iputStrLn banner

540− ist <- get

545+ ist <- getIState

541 mods <- mapM loadModule inputs

546 mods <- mapM loadModule inputs

542 ok <- noErrors

547 ok <- noErrors

543 when ok $ case output of

548 when ok $ case output of

@@ -546,7 +551,7 @@ idrisMain opts =

546 when ok $ case newoutput of

551 when ok $ case newoutput of

547 [] -> return ()

552 [] -> return ()

548 (o:_) -> process "" (NewCompile o)

553 (o:_) -> process "" (NewCompile o)

549− when runrepl $ repl ist inputs

554+ when runrepl $ runInputT replSettings $ repl ist inputs

550 ok <- noErrors

555 ok <- noErrors

551 when (not ok) $ liftIO (exitWith (ExitFailure 1))

556 when (not ok) $ liftIO (exitWith (ExitFailure 1))

552 where

557 where

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 (runIdris opts) idrisInit

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

45runIdris opts = do