git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1296 from david-christiansen/ide-prover

Correct IDESlave protocol violations in prover

commit5700be72104bbd53b83fe994691f22c0a25130fc authorDavid Christiansen <david@davidchristiansen.dk> dateSun 8 Jun 2014, 04:36 (12 years ago) parentdb929866d0abfb
2 files changed+32−14
compare with master
unifiedsplit
src/Idris/Prover.hs+13−9 src/Idris/REPL.hs+19−5
src/Idris/Prover.hs+13−9
@@ -63,9 +63,10 @@ prove opt ctxt lit n ty
6363 ideslavePutSExp "start-proof-mode" n
6464 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
6565 iLOG $ "Adding " ++ show tm
66− iputStrLn $ showProof lit n prf
6766 i <- getIState
68− ideslavePutSExp "end-proof-mode" n
67+ case idris_outputmode i of
68+ IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)
69+ _ -> iputStrLn $ showProof lit n prf
6970 let proofs = proof_list i
7071 putIState (i { proof_list = (n, prf) : proofs })
7172 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
@@ -85,6 +86,11 @@ prove opt ctxt lit n ty
8586 [([], P Ref n ty, ptm)]
8687 [([], P Ref n ty, ptm')] ty)
8788 solveDeferred n
89+ case idris_outputmode i of
90+ IdeSlave n ->
91+ runIO . putStrLn $
92+ convSExp "return" (SymbolAtom "ok", "") n
93+ _ -> return ()
8894
8995elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
9096elabStep st e = case runStateT eCheck st of
@@ -203,16 +209,14 @@ ploop fn d prompt prf e h
203209 Failure err -> do iPrintError (show err)
204210 return (False, e, False, prf)
205211 Success Undo -> do (_, st) <- elabStep e loadState
206− iPrintResult ""
207212 return (True, st, False, init prf)
208− Success ProofState -> do iPrintResult ""
209− return (True, e, False, prf)
213+ Success ProofState -> return (True, e, False, prf)
210214 Success ProofTerm -> do tm <- lifte e get_term
211− iPrintResult $ "TT: " ++ show tm ++ "\n"
215+ iputStrLn $ "TT: " ++ show tm ++ "\n"
212216 return (False, e, False, prf)
213217 Success Qed -> do hs <- lifte e get_holes
214218 when (not (null hs)) $ ifail "Incomplete proof"
215− iPrintResult "Proof completed!"
219+ iputStrLn "Proof completed!"
216220 return (False, e, True, prf)
217221 Success (TCheck (PRef _ n)) ->
218222 do ctxt <- getContext
@@ -277,12 +281,12 @@ ploop fn d prompt prf e h
277281 Success tac -> do (_, e) <- elabStep e saveState
278282 (_, st) <- elabStep e (runTac autoSolve i fn tac)
279283-- trace (show (problems (proof st))) $
280− iPrintResult ""
281284 return (True, st, False, prf ++ [step]))
282285 (\err -> do iPrintError (pshow i err)
283286 return (False, e, False, prf))
284287 ideslavePutSExp "write-proof-state" (prf', length prf')
285288 if done then do (tm, _) <- elabStep st get_term
286289 return (tm, prf')
287− else ploop fn d prompt prf' st h'
290+ else do iPrintResult ""
291+ ploop fn d prompt prf' st h'
288292 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
src/Idris/REPL.hs+19−5
@@ -240,11 +240,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
240240 i <- getIState
241241 case parseCmd i "(input)" cmd of
242242 Failure err -> iPrintError $ show (fixColour c err)
243− Success (Prove n') -> do iPrintResult ""
244− idrisCatch
245− (process stdout fn (Prove n'))
246− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
247− isetPrompt (mkPrompt mods)
243+ Success (Prove n') ->
244+ idrisCatch
245+ (do process stdout fn (Prove n')
246+ isetPrompt (mkPrompt mods)
247+ case idris_outputmode i of
248+ IdeSlave n -> -- signal completion of proof to ide
249+ runIO . hPutStrLn stdout $
250+ IdeSlave.convSExp "return"
251+ (IdeSlave.SymbolAtom "ok", "")
252+ n
253+ _ -> return ())
254+ (\e -> do ist <- getIState
255+ isetPrompt (mkPrompt mods)
256+ case idris_outputmode i of
257+ IdeSlave n ->
258+ runIO . hPutStrLn stdout $
259+ IdeSlave.convSExp "abandon-proof" "Abandoned" n
260+ _ -> return ()
261+ ihRenderError stdout $ pprintErr ist e)
248262 Success cmd -> idrisCatch
249263 (ideslaveProcess fn cmd)
250264 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)