git.iko.soy/Idris-dev
on master help sign in
send start/end proof mode messages from within prover
64afbf1Hannes Mehnert
src/Idris/Prover.hs+8−3
compare with master
unifiedsplit
@@ -53,18 +53,23 @@ assumptionNames e
53 names ((n, _) : bs) = show n : names bs
53 names ((n, _) : bs) = show n : names bs
54
54
55prove :: Context -> Bool -> Name -> Type -> Idris ()
55prove :: Context -> Bool -> Name -> Type -> Idris ()
56−prove ctxt lit n ty
56+prove ctxt lit n ty
57 = do let ps = initElaborator n ctxt ty
57 = 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 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
61 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
59 iLOG $ "Adding " ++ show tm
62 iLOG $ "Adding " ++ show tm
60 iputStrLn $ showProof lit n prf
63 iputStrLn $ showProof lit n prf
61 i <- getIState
64 i <- getIState
65+ case (idris_outputmode i) of
66+ IdeSlave id -> liftIO $ putStrLn $ convSExp "end-proof-mode" n id
62 let proofs = proof_list i
67 let proofs = proof_list i
63 putIState (i { proof_list = (n, prf) : proofs })
68 putIState (i { proof_list = (n, prf) : proofs })
64 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
69 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
65 logLvl 3 (show tree)
70 logLvl 3 (show tree)
66 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
71 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
67− logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
72+ logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
68 "Expected type:" ++ show ty)
73 "Expected type:" ++ show ty)
69 case converts ctxt [] ty pty of
74 case converts ctxt [] ty pty of
70 OK _ -> return ()
75 OK _ -> return ()
@@ -72,7 +77,7 @@ prove ctxt lit n ty
72 ptm' <- applyOpts ptm
77 ptm' <- applyOpts ptm
73 updateContext (addCasedef n True False True False
78 updateContext (addCasedef n True False True False
74 [Right (P Ref n ty, ptm)]
79 [Right (P Ref n ty, ptm)]
75− [([], P Ref n ty, ptm)]
80+ [([], P Ref n ty, ptm)]
76 [([], P Ref n ty, ptm')] ty)
81 [([], P Ref n ty, ptm')] ty)
77 solveDeferred n
82 solveDeferred n
78elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
83elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
src/Idris/REPL.hs−4
@@ -110,13 +110,9 @@ ideslave orig mods
110 case parseCmd i cmd of
110 case parseCmd i cmd of
111 Left err -> iFail $ show err
111 Left err -> iFail $ show err
112 Right (Prove n') -> do iResult ""
112 Right (Prove n') -> do iResult ""
113− liftIO $ putStrLn $ convSExp "proof-mode" (True, n') id
114 idrisCatch
113 idrisCatch
115 (do process fn (Prove n'))
114 (do process fn (Prove n'))
116 (\e -> do iFail $ show e)
115 (\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
120 isetPrompt (mkPrompt mods)
116 isetPrompt (mkPrompt mods)
121 Right cmd -> idrisCatch
117 Right cmd -> idrisCatch
122 (do ideslaveProcess fn cmd)
118 (do ideslaveProcess fn cmd)