40611be · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Implement CaseSplit in IdeSlave

40611beHannes Mehnert13 years ago

src/Idris/IdeSlave.hs+8−6

compare with master

unifiedsplit

@@ -94,16 +94,18 @@ parseSExp = parse pSExp "(unknown)"

94data IdeSlaveCommand = REPLCompletions String

95 | Interpret String

96 | TypeOf String

97+ | CaseSplit Int String

97 | LoadFile String

98 | LoadFile String

98 deriving Show

99 deriving Show

100

100sexpToCommand :: SExp -> Maybe IdeSlaveCommand

101sexpToCommand :: SExp -> Maybe IdeSlaveCommand

101−sexpToCommand (SexpList (x:[])) = sexpToCommand x

102+sexpToCommand (SexpList (x:[])) = sexpToCommand x

102−sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

103+sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

103−sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

104+sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

104−sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

105+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

105−sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

106+sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

106−sexpToCommand _ = Nothing

107+sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

108+sexpToCommand _ = Nothing

107

109

108parseMessage :: String -> Either Err (SExp, Integer)

110parseMessage :: String -> Either Err (SExp, Integer)

109parseMessage x = case receiveString x of

111parseMessage x = case receiveString x of

src/Idris/REPL.hs+21−19

@@ -17,7 +17,7 @@ import Idris.UnusedArgs

17import Idris.Docs

18import Idris.Help

19import Idris.Completion

20−import Idris.IdeSlave

20+import qualified Idris.IdeSlave as IdeSlave

21import Idris.Chaser

22import Idris.Imports

23import Idris.Colours

@@ -194,17 +194,17 @@ ideslave :: IState -> [FilePath] -> Idris ()

194ideslave orig mods

195 = do idrisCatch

196 (do l <- runIO $ getLine

197− (sexp, id) <- case parseMessage l of

197+ (sexp, id) <- case IdeSlave.parseMessage l of

198 Left err -> ierror err

199 Right (sexp, id) -> return (sexp, id)

200 i <- getIState

201 putIState $ i { idris_outputmode = (IdeSlave id) }

202+ let fn = case mods of

203+ (f:_) -> f

204+ _ -> ""

202− case sexpToCommand sexp of

205+ case IdeSlave.sexpToCommand sexp of

203− Just (Interpret cmd) ->

206+ Just (IdeSlave.Interpret cmd) ->

204− do let fn = case mods of

205− (f:_) -> f

206− _ -> ""

207− c <- colourise

207+ do c <- colourise

208 case parseCmd i "(input)" cmd of

209 Failure err -> iPrintError $ show (fixColour c err)

210 Success (Prove n') -> do iPrintResult ""

@@ -215,11 +215,11 @@ ideslave orig mods

215 Success cmd -> idrisCatch

216 (ideslaveProcess fn cmd)

217 (\e -> getIState >>= iPrintError . flip pshow e)

218− Just (REPLCompletions str) ->

218+ Just (IdeSlave.REPLCompletions str) ->

219 do (unused, compls) <- replCompletion (reverse str, "")

220− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

220+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

221− runIO $ putStrLn $ convSExp "return" good id

221+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

222− Just (LoadFile filename) ->

222+ Just (IdeSlave.LoadFile filename) ->

223 do clearErr

224 putIState (orig { idris_options = idris_options i,

225 idris_outputmode = (IdeSlave id) })

@@ -233,8 +233,10 @@ ideslave orig mods

233 Nothing -> iPrintResult $ "loaded " ++ filename

234 Just x -> iPrintError $ "didn't load " ++ filename

235 ideslave orig [filename]

236− Just (TypeOf name) ->

236+ Just (IdeSlave.TypeOf name) ->

237 process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238+ Just (IdeSlave.CaseSplit line name) ->

239+ process stdout fn (CaseSplitAt False line (UN name))

238 Nothing -> do iPrintError "did not understand")

240 Nothing -> do iPrintError "did not understand")

239 (\e -> do iPrintError $ show e)

241 (\e -> do iPrintError $ show e)

240 ideslave orig mods

242 ideslave orig mods

@@ -550,12 +552,12 @@ process h fn (CaseSplitAt updatefile l n)

550 let (before, (ap : later)) = splitAt (l-1) (lines src)

552 let (before, (ap : later)) = splitAt (l-1) (lines src)

551 res' <- replaceSplits ap res

553 res' <- replaceSplits ap res

552 let new = concat res'

554 let new = concat res'

553− if updatefile then

555+ if updatefile

554− do let fb = fn ++ "~" -- make a backup!

556+ then do let fb = fn ++ "~" -- make a backup!

555− runIO $ writeFile fb (unlines before ++ new ++ unlines later)

557+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)

556− runIO $ copyFile fb fn

558+ runIO $ copyFile fb fn

557− else -- do ihputStrLn h (show res)

559+ else -- do ihputStrLn h (show res)

558− ihputStrLn h new

560+ ihPrintResult h new

559process h fn (AddClauseFrom updatefile l n)

561process h fn (AddClauseFrom updatefile l n)

560 = do src <- runIO $ readFile fn

562 = do src <- runIO $ readFile fn

561 let (before, tyline : later) = splitAt (l-1) (lines src)

563 let (before, tyline : later) = splitAt (l-1) (lines src)