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

git.iko.soy/Idris-dev

cleanups

commit9b4b7dccffbd499feb4c1c49206f31e3121e2362 authorHannes Mehnert <hannes@mehnert.org> dateMon 15 Jul 2013, 10:45 (13 years ago) parent64afbf1

3 files changed+17−16

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+11−5 src/Idris/IdeSlave.hs+2−5 src/Idris/Prover.hs+4−6

src/Idris/AbsSyntax.hs+11−5

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

264264 s -> liftIO $ putStrLn s

265265 IdeSlave n ->

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

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

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

268268

269269iputStrLn :: String -> Idris ()

270270iputStrLn s = do i <- getIState

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

277277 ([], msg) -> write

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

279279 _ -> 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 ()

281287

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

283289iputGoal :: String -> Idris ()

284290iputGoal s = do i <- getIState

285291 case idris_outputmode i of

286292 RawOutput -> liftIO $ putStrLn s

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

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

288294

289295isetPrompt :: String -> Idris ()

290296isetPrompt p = do i <- getIState

291297 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

293299

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

295301iWarn fc err = do i <- getIState

296302 case idris_outputmode i of

297303 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

299305

300306setLogLevel :: Int -> Idris ()

301307setLogLevel l = do i <- getIState

src/Idris/IdeSlave.hs+2−5

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

11{-# 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

55import Text.Printf

66import Numeric

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

4646

4747

4848instance SExpable Name where

49− toSExp (UN s) = SexpList [SymbolAtom "UN", StringAtom 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"]

49+ toSExp s = StringAtom (show s)

5350

5451

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

src/Idris/Prover.hs+4−6

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

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

5656prove ctxt lit n ty

5757 = do let ps = initElaborator n ctxt ty

58− i <- getIState

59− case (idris_outputmode i) of

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

58+ ideslavePutSExp "start-proof-mode" n

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

6260 iLOG $ "Adding " ++ show tm

6361 iputStrLn $ showProof lit n prf

6462 i <- getIState

65− case (idris_outputmode i) of

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

63+ ideslavePutSExp "end-proof-mode" n

6764 let proofs = proof_list i

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

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

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

143140 Just (REPLCompletions prefix) ->

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

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

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

143+ ideslavePutSExp "return" good

147144 receiveInput e

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

149146 Nothing -> return Nothing

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

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

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

197194 return (False, e, False, prf))

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

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

199197 return (tm, prf')

200198 else ploop d prompt prf' st h'