0970f01 · Idris-dev · git.iko.soy

src/Core/ProofShell.hs+18−16

compare with master

unifiedsplit

@@ -58,20 +58,22 @@ processCommand (Tac e) state

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

59

60runShell :: ShellState -> Idris ShellState

61+runShell st = runInputT defaultSettings $ runShell' st

62+ where

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

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

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

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

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

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

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

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

65− (prf st)

67+ (prf st)

66− x <- getInputLine prompt

68+ x <- getInputLine prompt

67− cmd <- case x of

69+ cmd <- case x of

68− Nothing -> return $ Right Quit

70+ Nothing -> return $ Right Quit

69− Just input -> return (parser input)

71+ Just input -> return (parser input)

70− case cmd of

72+ case cmd of

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

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

72− runShell st

74+ runShell' st

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

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

74− outputStrLn r

76+ outputStrLn r

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

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

76− else return st'

78+ else return st'

77

79

src/Idris/AbsSyntax.hs+2−2

@@ -148,10 +148,10 @@ setSO s = do i <- getIState

148 putIState $ (i { compiled_so = s })

149

150getIState :: Idris IState

151−getIState = lift get

151+getIState = get

152

153putIState :: IState -> Idris ()

154−putIState = lift . put

154+putIState = put

155

156getName :: Idris Int

157getName = do i <- getIState;

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 = InputT (StateT IState IO)

139+type Idris = StateT IState IO

140

141-- Commands in the REPL

142

src/Idris/Prover.hs+7−5

@@ -37,10 +37,12 @@ showProof lit n ps

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

38 break = "\n" ++ bird

39

40+proverSettings = defaultSettings -- TODO: Prover settings

41+

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

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

41prove ctxt lit n ty

43prove ctxt lit n ty

42 = do let ps = initElaborator n ctxt ty

44 = do let ps = initElaborator n ctxt ty

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

45+ (tm, prf) <- runInputT proverSettings $ ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)

44 iLOG $ "Adding " ++ show tm

46 iLOG $ "Adding " ++ show tm

45 iputStrLn $ showProof lit n prf

47 iputStrLn $ showProof lit n prf

46 i <- getIState

48 i <- getIState

@@ -108,9 +110,9 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a

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

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

109 return v

111 return v

110

112

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

113+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> InputT Idris (Term, [String])

112ploop d prompt prf e

114ploop d prompt prf e

113− = do i <- getIState

115+ = do i <- lift getIState

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

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

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

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

116 (cmd, step) <- case x of

118 (cmd, step) <- case x of

@@ -119,7 +121,7 @@ ploop d prompt prf e

119 case cmd of

121 case cmd of

120 Right Abandon -> fail "Abandoned"

122 Right Abandon -> fail "Abandoned"

121 _ -> return ()

123 _ -> return ()

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

124+ (d, st, done, prf') <- lift $ idrisCatch

123 (case cmd of

125 (case cmd of

124 Left err -> do iputStrLn (show err)

126 Left err -> do iputStrLn (show err)

125 return (False, e, False, prf)

127 return (False, e, False, prf)

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

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

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

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

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

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

144 return (False, e, False, prf))

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

145+ if done then do (tm, _) <- lift $ elabStep st get_term

144 return (tm, prf')

146 return (tm, prf')

145 else ploop d prompt prf' st

147 else ploop d prompt prf' st

146

148

src/Idris/REPL.hs+7−7

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

50import Data.Char

51import Data.Version

52

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

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

54repl orig mods

55 = H.catch

56 (do let prompt = mkPrompt mods

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

58 case x of

59− Nothing -> do iputStrLn "Bye bye"

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

60 return ()

61 Just input -> H.catch

62− (do ms <- processInput input orig mods

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

63 case ms of

64 Just mods -> repl orig mods

65 Nothing -> return ())

66 ctrlC)

67 ctrlC

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

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

69− ctrlC e = do iputStrLn (show e)

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

70 repl orig mods

71

72mkPrompt [] = "Idris"

@@ -496,7 +496,7 @@ haskelineSettings = setComplete idrisCompletion defaultSettings

496

497-- invoke as if from command line

498idris :: [Opt] -> IO IState

499−idris opts = execStateT (runInputT haskelineSettings $ idrisMain opts) idrisInit

499+idris opts = execStateT (idrisMain opts) idrisInit

500

501--runInputT haskelineSettings $ execStateT (idrisMain opts) idrisInit

502

@@ -553,7 +553,7 @@ idrisMain opts =

553 when ok $ case newoutput of

554 [] -> return ()

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

556− when runrepl $ repl ist inputs

556+ when runrepl $ runInputT haskelineSettings $ repl ist inputs

557 ok <- noErrors

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

559 where

src/Main.hs+1−1

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

39

40main = do xs <- getArgs

41 let opts = parseArgs xs

42− execStateT (runInputT haskelineSettings $ runIdris opts) idrisInit

42+ execStateT (runIdris opts) idrisInit

43

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

45runIdris opts = do