9b4b7dc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

cleanups

9b4b7dcHannes Mehnert13 years ago

src/Idris/AbsSyntax.hs+11−5

compare with master

unifiedsplit

@@ -264,7 +264,7 @@ iFail s = do i <- getIState

264 s -> liftIO $ putStrLn s

265 IdeSlave n ->

266 let good = SexpList [SymbolAtom "error", toSExp s] in

267− liftIO $ putStrLn $ convSExp "return" good n

267+ liftIO . putStrLn $ convSExp "return" good n

268

269iputStrLn :: String -> Idris ()

270iputStrLn s = do i <- getIState

@@ -277,25 +277,31 @@ iputStrLn s = do i <- getIState

277 ([], msg) -> write

278 (num, ':':msg) -> iWarn (FC fn (read num)) msg

279 _ -> write

280− where write = liftIO $ putStrLn $ convSExp "write-string" s n

280+ where write = liftIO . putStrLn $ convSExp "write-string" s n

281+

282+ideslavePutSExp :: SExpable a => String -> a -> Idris ()

283+ideslavePutSExp cmd info = do i <- getIState

284+ case idris_outputmode i of

285+ IdeSlave n -> liftIO . putStrLn $ convSExp cmd info n

286+ _ -> return ()

281

287

282-- this needs some typing magic and more structured output towards emacs

288-- this needs some typing magic and more structured output towards emacs

283iputGoal :: String -> Idris ()

289iputGoal :: String -> Idris ()

284iputGoal s = do i <- getIState

290iputGoal s = do i <- getIState

285 case idris_outputmode i of

291 case idris_outputmode i of

286 RawOutput -> liftIO $ putStrLn s

292 RawOutput -> liftIO $ putStrLn s

287− IdeSlave n -> liftIO $ putStrLn $ convSExp "write-goal" s n

293+ IdeSlave n -> liftIO . putStrLn $ convSExp "write-goal" s n

288

294

289isetPrompt :: String -> Idris ()

295isetPrompt :: String -> Idris ()

290isetPrompt p = do i <- getIState

296isetPrompt p = do i <- getIState

291 case idris_outputmode i of

297 case idris_outputmode i of

292− IdeSlave n -> liftIO $ putStrLn $ convSExp "set-prompt" p n

298+ IdeSlave n -> liftIO . putStrLn $ convSExp "set-prompt" p n

293

299

294iWarn :: FC -> String -> Idris ()

300iWarn :: FC -> String -> Idris ()

295iWarn fc err = do i <- getIState

301iWarn fc err = do i <- getIState

296 case idris_outputmode i of

302 case idris_outputmode i of

297 RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)

303 RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)

298− IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

304+ IdeSlave n -> liftIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

299

305

300setLogLevel :: Int -> Idris ()

306setLogLevel :: Int -> Idris ()

301setLogLevel l = do i <- getIState

307setLogLevel l = do i <- getIState

src/Idris/IdeSlave.hs+2−5

@@ -1,6 +1,6 @@

1{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

3−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..)) where

3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable) where

5import Text.Printf

6import Numeric

@@ -46,10 +46,7 @@ instance SExpable Int where

48instance SExpable Name where

49− toSExp (UN s) = SexpList [SymbolAtom "UN", StringAtom s]

49+ toSExp s = StringAtom (show s)

50− toSExp (NS s ns) = SexpList [SymbolAtom "NS", toSExp s, toSExp ns]

51− toSExp (MN n s) = SexpList [SymbolAtom "MN", toSExp n, toSExp s]

52− toSExp NErased = SexpList [SymbolAtom "NErased"]

55instance (SExpable a) => SExpable (Maybe a) where

52instance (SExpable a) => SExpable (Maybe a) where

src/Idris/Prover.hs+4−6

@@ -55,15 +55,12 @@ assumptionNames e

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

56prove ctxt lit n ty

57 = do let ps = initElaborator n ctxt ty

58− i <- getIState

58+ ideslavePutSExp "start-proof-mode" n

59− case (idris_outputmode i) of

60− IdeSlave id -> liftIO $ putStrLn $ convSExp "start-proof-mode" n id

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

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

62 iLOG $ "Adding " ++ show tm

60 iLOG $ "Adding " ++ show tm

63 iputStrLn $ showProof lit n prf

61 iputStrLn $ showProof lit n prf

64 i <- getIState

62 i <- getIState

65− case (idris_outputmode i) of

63+ ideslavePutSExp "end-proof-mode" n

66− IdeSlave id -> liftIO $ putStrLn $ convSExp "end-proof-mode" n id

67 let proofs = proof_list i

64 let proofs = proof_list i

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

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

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

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

@@ -143,7 +140,7 @@ receiveInput e =

143 Just (REPLCompletions prefix) ->

140 Just (REPLCompletions prefix) ->

144 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

141 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

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

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

146− liftIO $ putStrLn $ convSExp "return" good id

143+ ideslavePutSExp "return" good

147 receiveInput e

144 receiveInput e

148 Just (Interpret cmd) -> return (Just cmd)

145 Just (Interpret cmd) -> return (Just cmd)

149 Nothing -> return Nothing

146 Nothing -> return Nothing

@@ -195,6 +192,7 @@ ploop d prompt prf e h

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

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

196 (\err -> do iFail (show err)

193 (\err -> do iFail (show err)

197 return (False, e, False, prf))

194 return (False, e, False, prf))

195+ ideslavePutSExp "write-proof-state" (prf', length prf')

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

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

199 return (tm, prf')

197 return (tm, prf')

200 else ploop d prompt prf' st h'

198 else ploop d prompt prf' st h'