@@ -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
@@ -171,7 +177,7 @@ receiveInput e =
171177 ideslavePutSExp "return" good
172178 receiveInput e
173179 Just (Interpret cmd) -> return (Just cmd)
174− Nothing -> return Nothing
180+ _ -> return Nothing
175181
176182ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
177183ploop fn d prompt prf e h
@@ -198,91 +204,95 @@ ploop fn d prompt prf e h
198204 case cmd of
199205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
200206 _ -> return ()
201− (d, st, done, prf') <- idrisCatch
207+ (d, st, done, prf', res) <- idrisCatch
202208 (case cmd of
203− Failure err -> do iPrintError (show err)
204− return (False, e, False, prf)
209+ Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
205210 Success Undo -> do (_, st) <- elabStep e loadState
206− iPrintResult ""
207− return (True, st, False, init prf)
208− Success ProofState -> do iPrintResult ""
209− return (True, e, False, prf)
211+ return (True, st, False, init prf, Right "")
212+ Success ProofState -> return (True, e, False, prf, Right "")
210213 Success ProofTerm -> do tm <- lifte e get_term
211− iPrintResult $ "TT: " ++ show tm ++ "\n"
212− return (False, e, False, prf)
214+ iputStrLn $ "TT: " ++ show tm ++ "\n"
215+ return (False, e, False, prf, Right "")
213216 Success Qed -> do hs <- lifte e get_holes
214217 when (not (null hs)) $ ifail "Incomplete proof"
215− iPrintResult "Proof completed!"
216− return (False, e, True, prf)
217− Success (TCheck (PRef _ n)) ->
218− do ctxt <- getContext
219− ist <- getIState
220− imp <- impShow
221− idrisCatch (do
222− let h = idris_outh ist
223− OK env = envAtFocus (proof e)
224− ctxt' = envCtxt env ctxt
225− bnd = map (\x -> (fst x, False)) env
226− ist' = ist { tt_ctxt = ctxt' }
227− putIState ist'
228− -- Unlike the REPL, metavars have no special treatment, to
229− -- make it easier to see how to prove with them.
230− case lookupNames n ctxt' of
231− [] -> ihPrintError h $ "No such variable " ++ show n
232− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
233− putIState ist
234− return (False, e, False, prf))
235− (\err -> do putIState ist ; ierror err)
236− Success (TCheck t) ->
237− do ist <- getIState
238− ctxt <- getContext
239− idrisCatch (do
240− let OK env = envAtFocus (proof e)
241− ctxt' = envCtxt env ctxt
242− putIState ist { tt_ctxt = ctxt' }
243− (tm, ty) <- elabVal toplevel False t
244− let ppo = ppOptionIst ist
245− ty' = normaliseC ctxt [] ty
246− h = idris_outh ist
247− infixes = idris_infixes ist
248− case tm of
249− TType _ ->
250− ihPrintTermWithType h (prettyImp ppo PType) type1Doc
251− _ -> let bnd = map (\x -> (fst x, False)) env in
252− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
253− (pprintPTerm ppo bnd [] infixes (delab ist ty))
254− putIState ist
255− return (False, e, False, prf))
256− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
257− Success (TEval t) -> withErrorReflection $
258− do ctxt <- getContext
259− ist <- getIState
260− idrisCatch (do
261− let OK env = envAtFocus (proof e)
262− ctxt' = envCtxt env ctxt
263− ist' = ist { tt_ctxt = ctxt' }
264− bnd = map (\x -> (fst x, False)) env
265− putIState ist'
266− (tm, ty) <- elabVal toplevel False t
267− let tm' = force (normaliseAll ctxt' env tm)
268− ty' = force (normaliseAll ctxt' env ty)
269− ppo = ppOption (idris_options ist')
270− infixes = idris_infixes ist
271− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
272− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
273− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
274− putIState ist
275− return (False, e, False, prf))
276− (\err -> do putIState ist ; ierror err)
218+ iputStrLn "Proof completed!"
219+ return (False, e, True, prf, Right "")
220+ Success (TCheck (PRef _ n)) -> checkNameType n
221+ Success (TCheck t) -> checkType t
222+ Success (TEval t) -> evalTerm t e
277223 Success tac -> do (_, e) <- elabStep e saveState
278224 (_, st) <- elabStep e (runTac autoSolve i fn tac)
279−-- trace (show (problems (proof st))) $
280− iPrintResult ""
281− return (True, st, False, prf ++ [step]))
282− (\err -> do iPrintError (pshow i err)
283− return (False, e, False, prf))
225+ return (True, st, False, prf ++ [step], Right ""))
226+ (\err -> return (False, e, False, prf, Left err))
284227 ideslavePutSExp "write-proof-state" (prf', length prf')
285− if done then do (tm, _) <- elabStep st get_term
286− return (tm, prf')
287− else ploop fn d prompt prf' st h'
228+ case res of
229+ Left err -> do iPrintError (pshow i err)
230+ ploop fn d prompt prf' st h'
231+ Right ok ->
232+ if done then do (tm, _) <- elabStep st get_term
233+ return (tm, prf')
234+ else do iPrintResult ok
235+ ploop fn d prompt prf' st h'
288236 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
237+ checkNameType n = do
238+ ctxt <- getContext
239+ ist <- getIState
240+ imp <- impShow
241+ idrisCatch (do
242+ let h = idris_outh ist
243+ OK env = envAtFocus (proof e)
244+ ctxt' = envCtxt env ctxt
245+ bnd = map (\x -> (fst x, False)) env
246+ ist' = ist { tt_ctxt = ctxt' }
247+ putIState ist'
248+ -- Unlike the REPL, metavars have no special treatment, to
249+ -- make it easier to see how to prove with them.
250+ case lookupNames n ctxt' of
251+ [] -> ihPrintError h $ "No such variable " ++ show n
252+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
253+ putIState ist
254+ return (False, e, False, prf, Right ""))
255+ (\err -> do putIState ist ; ierror err)
256+
257+ checkType t = do
258+ ist <- getIState
259+ ctxt <- getContext
260+ idrisCatch (do
261+ let OK env = envAtFocus (proof e)
262+ ctxt' = envCtxt env ctxt
263+ putIState ist { tt_ctxt = ctxt' }
264+ (tm, ty) <- elabVal toplevel False t
265+ let ppo = ppOptionIst ist
266+ ty' = normaliseC ctxt [] ty
267+ h = idris_outh ist
268+ infixes = idris_infixes ist
269+ case tm of
270+ TType _ ->
271+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
272+ _ -> let bnd = map (\x -> (fst x, False)) env in
273+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
274+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
275+ putIState ist
276+ return (False, e, False, prf, Right ""))
277+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
278+
279+ evalTerm t e = withErrorReflection $
280+ do ctxt <- getContext
281+ ist <- getIState
282+ idrisCatch (do
283+ let OK env = envAtFocus (proof e)
284+ ctxt' = envCtxt env ctxt
285+ ist' = ist { tt_ctxt = ctxt' }
286+ bnd = map (\x -> (fst x, False)) env
287+ putIState ist'
288+ (tm, ty) <- elabVal toplevel False t
289+ let tm' = force (normaliseAll ctxt' env tm)
290+ ty' = force (normaliseAll ctxt' env ty)
291+ ppo = ppOption (idris_options ist')
292+ infixes = idris_infixes ist
293+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
294+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
295+ ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
296+ putIState ist
297+ return (False, e, False, prf, Right ""))
298+ (\err -> do putIState ist ; ierror err)