git.iko.soy/Idris-dev
on master help sign in
send start/end proof mode messages from within prover
commit64afbf1adb40f712685778c16de049e568276055 authorHannes Mehnert <hannes@mehnert.org> dateTue 21 May 2013, 14:34 (13 years ago) parent1721a22
2 files changed+8−7
compare with master
unifiedsplit
src/Idris/Prover.hs+8−3 src/Idris/REPL.hs−4
src/Idris/Prover.hs+8−3
@@ -53,18 +53,23 @@ assumptionNames e
5353 names ((n, _) : bs) = show n : names bs
5454
5555prove :: Context -> Bool -> Name -> Type -> Idris ()
56−prove ctxt lit n ty
56+prove 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
5861 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
5962 iLOG $ "Adding " ++ show tm
6063 iputStrLn $ showProof lit n prf
6164 i <- getIState
65+ case (idris_outputmode i) of
66+ IdeSlave id -> liftIO $ putStrLn $ convSExp "end-proof-mode" n id
6267 let proofs = proof_list i
6368 putIState (i { proof_list = (n, prf) : proofs })
6469 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
6570 logLvl 3 (show tree)
6671 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
67− logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
72+ logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
6873 "Expected type:" ++ show ty)
6974 case converts ctxt [] ty pty of
7075 OK _ -> return ()
@@ -72,7 +77,7 @@ prove ctxt lit n ty
7277 ptm' <- applyOpts ptm
7378 updateContext (addCasedef n True False True False
7479 [Right (P Ref n ty, ptm)]
75− [([], P Ref n ty, ptm)]
80+ [([], P Ref n ty, ptm)]
7681 [([], P Ref n ty, ptm')] ty)
7782 solveDeferred n
7883elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
src/Idris/REPL.hs−4
@@ -110,13 +110,9 @@ ideslave orig mods
110110 case parseCmd i cmd of
111111 Left err -> iFail $ show err
112112 Right (Prove n') -> do iResult ""
113− liftIO $ putStrLn $ convSExp "proof-mode" (True, n') id
114113 idrisCatch
115114 (do process fn (Prove n'))
116115 (\e -> do iFail $ show e)
117− i <- getIState
118− case (idris_outputmode i) of
119− IdeSlave id -> liftIO $ putStrLn $ convSExp "proof-mode" (False, n') id
120116 isetPrompt (mkPrompt mods)
121117 Right cmd -> idrisCatch
122118 (do ideslaveProcess fn cmd)