@@ -218,66 +218,9 @@ ploop fn d prompt prf e h
218218 when (not (null hs)) $ ifail "Incomplete proof"
219219 iputStrLn "Proof completed!"
220220 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)
221+ Success (TCheck (PRef _ n)) -> checkNameType n
222+ Success (TCheck t) -> checkType t
223+ Success (TEval t) -> evalTerm t e
281224 Success tac -> do (_, e) <- elabStep e saveState
282225 (_, st) <- elabStep e (runTac autoSolve i fn tac)
283226-- trace (show (problems (proof st))) $
@@ -290,3 +233,65 @@ ploop fn d prompt prf e h
290233 else do iPrintResult ""
291234 ploop fn d prompt prf' st h'
292235 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
236+ checkNameType n = do
237+ ctxt <- getContext
238+ ist <- getIState
239+ imp <- impShow
240+ idrisCatch (do
241+ let h = idris_outh ist
242+ OK env = envAtFocus (proof e)
243+ ctxt' = envCtxt env ctxt
244+ bnd = map (\x -> (fst x, False)) env
245+ ist' = ist { tt_ctxt = ctxt' }
246+ putIState ist'
247+ -- Unlike the REPL, metavars have no special treatment, to
248+ -- make it easier to see how to prove with them.
249+ case lookupNames n ctxt' of
250+ [] -> ihPrintError h $ "No such variable " ++ show n
251+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
252+ putIState ist
253+ return (False, e, False, prf))
254+ (\err -> do putIState ist ; ierror err)
255+
256+ checkType t = do
257+ ist <- getIState
258+ ctxt <- getContext
259+ idrisCatch (do
260+ let OK env = envAtFocus (proof e)
261+ ctxt' = envCtxt env ctxt
262+ putIState ist { tt_ctxt = ctxt' }
263+ (tm, ty) <- elabVal toplevel False t
264+ let ppo = ppOptionIst ist
265+ ty' = normaliseC ctxt [] ty
266+ h = idris_outh ist
267+ infixes = idris_infixes ist
268+ case tm of
269+ TType _ ->
270+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
271+ _ -> let bnd = map (\x -> (fst x, False)) env in
272+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
273+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
274+ putIState ist
275+ return (False, e, False, prf))
276+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
277+
278+ evalTerm t e = withErrorReflection $
279+ do ctxt <- getContext
280+ ist <- getIState
281+ idrisCatch (do
282+ let OK env = envAtFocus (proof e)
283+ ctxt' = envCtxt env ctxt
284+ ist' = ist { tt_ctxt = ctxt' }
285+ bnd = map (\x -> (fst x, False)) env
286+ putIState ist'
287+ (tm, ty) <- elabVal toplevel False t
288+ let tm' = force (normaliseAll ctxt' env tm)
289+ ty' = force (normaliseAll ctxt' env ty)
290+ ppo = ppOption (idris_options ist')
291+ infixes = idris_infixes ist
292+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
293+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
294+ ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
295+ putIState ist
296+ return (False, e, False, prf))
297+ (\err -> do putIState ist ; ierror err)