@@ -204,89 +204,95 @@ ploop fn d prompt prf e h
204204 case cmd of
205205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
206206 _ -> return ()
207− (d, st, done, prf') <- idrisCatch
207+ (d, st, done, prf', res) <- idrisCatch
208208 (case cmd of
209− Failure err -> do iPrintError (show err)
210− return (False, e, False, prf)
209+ Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
211210 Success Undo -> do (_, st) <- elabStep e loadState
212− return (True, st, False, init prf)
213− Success ProofState -> return (True, e, False, prf)
211+ return (True, st, False, init prf, Right "")
212+ Success ProofState -> return (True, e, False, prf, Right "")
214213 Success ProofTerm -> do tm <- lifte e get_term
215214 iputStrLn $ "TT: " ++ show tm ++ "\n"
216− return (False, e, False, prf)
215+ return (False, e, False, prf, Right "")
217216 Success Qed -> do hs <- lifte e get_holes
218217 when (not (null hs)) $ ifail "Incomplete proof"
219218 iputStrLn "Proof completed!"
220− return (False, e, True, prf)
221− Success (TCheck (PRef _ n)) ->
222− do ctxt <- getContext
223− ist <- getIState
224− imp <- impShow
225− idrisCatch (do
226− let h = idris_outh ist
227− OK env = envAtFocus (proof e)
228− ctxt' = envCtxt env ctxt
229− bnd = map (\x -> (fst x, False)) env
230− ist' = ist { tt_ctxt = ctxt' }
231− putIState ist'
232− -- Unlike the REPL, metavars have no special treatment, to
233− -- make it easier to see how to prove with them.
234− case lookupNames n ctxt' of
235− [] -> ihPrintError h $ "No such variable " ++ show n
236− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
237− putIState ist
238− return (False, e, False, prf))
239− (\err -> do putIState ist ; ierror err)
240− Success (TCheck t) ->
241− do ist <- getIState
242− ctxt <- getContext
243− idrisCatch (do
244− let OK env = envAtFocus (proof e)
245− ctxt' = envCtxt env ctxt
246− putIState ist { tt_ctxt = ctxt' }
247− (tm, ty) <- elabVal toplevel False t
248− let ppo = ppOptionIst ist
249− ty' = normaliseC ctxt [] ty
250− h = idris_outh ist
251− infixes = idris_infixes ist
252− case tm of
253− TType _ ->
254− ihPrintTermWithType h (prettyImp ppo PType) type1Doc
255− _ -> let bnd = map (\x -> (fst x, False)) env in
256− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
257− (pprintPTerm ppo bnd [] infixes (delab ist ty))
258− putIState ist
259− return (False, e, False, prf))
260− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
261− Success (TEval t) -> withErrorReflection $
262− do ctxt <- getContext
263− ist <- getIState
264− idrisCatch (do
265− let OK env = envAtFocus (proof e)
266− ctxt' = envCtxt env ctxt
267− ist' = ist { tt_ctxt = ctxt' }
268− bnd = map (\x -> (fst x, False)) env
269− putIState ist'
270− (tm, ty) <- elabVal toplevel False t
271− let tm' = force (normaliseAll ctxt' env tm)
272− ty' = force (normaliseAll ctxt' env ty)
273− ppo = ppOption (idris_options ist')
274− infixes = idris_infixes ist
275− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
276− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
277− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
278− putIState ist
279− return (False, e, False, prf))
280− (\err -> do putIState ist ; ierror err)
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
281223 Success tac -> do (_, e) <- elabStep e saveState
282224 (_, st) <- elabStep e (runTac autoSolve i fn tac)
283−-- trace (show (problems (proof st))) $
284− return (True, st, False, prf ++ [step]))
285− (\err -> do iPrintError (pshow i err)
286− return (False, e, False, prf))
225+ return (True, st, False, prf ++ [step], Right ""))
226+ (\err -> return (False, e, False, prf, Left err))
287227 ideslavePutSExp "write-proof-state" (prf', length prf')
288− if done then do (tm, _) <- elabStep st get_term
289− return (tm, prf')
290− else do iPrintResult ""
291− 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'
292236 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)