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

git.iko.soy/Idris-dev

Disentangle Haskeline from the internals Idris

Now, only the areas that actually work with the user involve the InputT monad transformer. The practical advantage of this is that different Haskeline settings structures can be used for different shells - the main REPL, the prover, and the TT shell, simply by providing a different completion function in the runInputT call.

commit0970f01da5351f172c24370e08c9361d376c6a01 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 11 Feb 2013, 15:18 (14 years ago) parentcc3c913

6 files changed+36−32

compare with master

unifiedsplit

src/Core/ProofShell.hs+18−16 src/Idris/AbsSyntax.hs+2−2 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Prover.hs+7−5 src/Idris/REPL.hs+7−7 src/Main.hs+1−1

src/Core/ProofShell.hs+18−16

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

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

5959

6060runShell :: ShellState -> Idris ShellState

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

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

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

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

65− (prf st)

66− x <- getInputLine prompt

67− cmd <- case x of

68− Nothing -> return $ Right Quit

69− Just input -> return (parser input)

70− case cmd of

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

72− runShell st

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

74− outputStrLn r

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

76− else return st'

61+runShell st = runInputT defaultSettings $ runShell' st

62+ where

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

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

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

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

67+ (prf st)

68+ x <- getInputLine prompt

69+ cmd <- case x of

70+ Nothing -> return $ Right Quit

71+ Just input -> return (parser input)

72+ case cmd of

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

74+ runShell' st

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

76+ outputStrLn r

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

78+ else return st'

7779

src/Idris/AbsSyntax.hs+2−2

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

148148 putIState $ (i { compiled_so = s })

149149

150150getIState :: Idris IState

151−getIState = lift get

151+getIState = get

152152

153153putIState :: IState -> Idris ()

154−putIState = lift . put

154+putIState = put

155155

156156getName :: Idris Int

157157getName = do i <- getIState;

src/Idris/AbsSyntaxTree.hs+1−1

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

136136

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

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

139−type Idris = InputT (StateT IState IO)

139+type Idris = StateT IState IO

140140

141141-- Commands in the REPL

142142

src/Idris/Prover.hs+7−5

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

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

3838 break = "\n" ++ bird

3939

40+proverSettings = defaultSettings -- TODO: Prover settings

41+

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

4143prove ctxt lit n ty

4244 = 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)

4446 iLOG $ "Adding " ++ show tm

4547 iputStrLn $ showProof lit n prf

4648 i <- getIState

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

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

109111 return v

110112

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

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

112114ploop d prompt prf e

113− = do i <- getIState

115+ = do i <- lift getIState

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

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

116118 (cmd, step) <- case x of

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

119121 case cmd of

120122 Right Abandon -> fail "Abandoned"

121123 _ -> return ()

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

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

123125 (case cmd of

124126 Left err -> do iputStrLn (show err)

125127 return (False, e, False, prf)

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

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

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

142144 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

144146 return (tm, prf')

145147 else ploop d prompt prf' st

146148

src/Idris/REPL.hs+7−7

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

5050import Data.Char

5151import Data.Version

5252

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

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

5454repl orig mods

5555 = H.catch

5656 (do let prompt = mkPrompt mods

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

5858 case x of

59− Nothing -> do iputStrLn "Bye bye"

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

6060 return ()

6161 Just input -> H.catch

62− (do ms <- processInput input orig mods

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

6363 case ms of

6464 Just mods -> repl orig mods

6565 Nothing -> return ())

6666 ctrlC)

6767 ctrlC

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

69− ctrlC e = do iputStrLn (show e)

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

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

7070 repl orig mods

7171

7272mkPrompt [] = "Idris"

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

496496

497497-- invoke as if from command line

498498idris :: [Opt] -> IO IState

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

499+idris opts = execStateT (idrisMain opts) idrisInit

500500

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

502502

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

553553 when ok $ case newoutput of

554554 [] -> return ()

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

556− when runrepl $ repl ist inputs

556+ when runrepl $ runInputT haskelineSettings $ repl ist inputs

557557 ok <- noErrors

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

559559 where

src/Main.hs+1−1

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

3939

4040main = do xs <- getArgs

4141 let opts = parseArgs xs

42− execStateT (runInputT haskelineSettings $ runIdris opts) idrisInit

42+ execStateT (runIdris opts) idrisInit

4343

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

4545runIdris opts = do