@@ -180,6 +180,7 @@ receiveInput e =
180 ideslavePutSExp "return" good
180 ideslavePutSExp "return" good
181 receiveInput e
181 receiveInput e
182 Just (Interpret cmd) -> return (Just cmd)
182 Just (Interpret cmd) -> return (Just cmd)
183+ Just (TypeOf str) -> return (Just (":t " ++ str))
183 _ -> return Nothing
184 _ -> return Nothing
185ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
186ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
@@ -211,21 +212,21 @@ ploop fn d prompt prf e h
211 (case cmd of
212 (case cmd of
212 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
213 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
213 Success Undo -> do (_, st) <- elabStep e loadState
214 Success Undo -> do (_, st) <- elabStep e loadState
214− return (True, st, False, init prf, Right "")
215+ return (True, st, False, init prf, Right $ iPrintResult "")
215− Success ProofState -> return (True, e, False, prf, Right "")
216+ Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
216 Success ProofTerm -> do tm <- lifte e get_term
217 Success ProofTerm -> do tm <- lifte e get_term
217 iputStrLn $ "TT: " ++ show tm ++ "\n"
218 iputStrLn $ "TT: " ++ show tm ++ "\n"
218− return (False, e, False, prf, Right "")
219+ return (False, e, False, prf, Right $ iPrintResult "")
219 Success Qed -> do hs <- lifte e get_holes
220 Success Qed -> do hs <- lifte e get_holes
220 when (not (null hs)) $ ifail "Incomplete proof"
221 when (not (null hs)) $ ifail "Incomplete proof"
221 iputStrLn "Proof completed!"
222 iputStrLn "Proof completed!"
222− return (False, e, True, prf, Right "")
223+ return (False, e, True, prf, Right $ iPrintResult "")
223 Success (TCheck (PRef _ n)) -> checkNameType n
224 Success (TCheck (PRef _ n)) -> checkNameType n
224 Success (TCheck t) -> checkType t
225 Success (TCheck t) -> checkType t
225 Success (TEval t) -> evalTerm t e
226 Success (TEval t) -> evalTerm t e
226 Success tac -> do (_, e) <- elabStep e saveState
227 Success tac -> do (_, e) <- elabStep e saveState
227 (_, st) <- elabStep e (runTac autoSolve i fn tac)
228 (_, st) <- elabStep e (runTac autoSolve i fn tac)
228− return (True, st, False, prf ++ [step], Right ""))
229+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
229 (\err -> return (False, e, False, prf, Left err))
230 (\err -> return (False, e, False, prf, Left err))
230 ideslavePutSExp "write-proof-state" (prf', length prf')
231 ideslavePutSExp "write-proof-state" (prf', length prf')
231 case res of
232 case res of
@@ -234,7 +235,7 @@ ploop fn d prompt prf e h
234 Right ok ->
235 Right ok ->
235 if done then do (tm, _) <- elabStep st get_term
236 if done then do (tm, _) <- elabStep st get_term
236 return (tm, prf')
237 return (tm, prf')
237− else do iPrintResult ok
238+ else do ok
238 ploop fn d prompt prf' st h'
239 ploop fn d prompt prf' st h'
239 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
240 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
240 checkNameType n = do
241 checkNameType n = do
@@ -250,11 +251,11 @@ ploop fn d prompt prf e h
250 putIState ist'
251 putIState ist'
251 -- Unlike the REPL, metavars have no special treatment, to
252 -- Unlike the REPL, metavars have no special treatment, to
252 -- make it easier to see how to prove with them.
253 -- make it easier to see how to prove with them.
253− case lookupNames n ctxt' of
254+ let action = case lookupNames n ctxt' of
254− [] -> ihPrintError h $ "No such variable " ++ show n
255+ [] -> ihPrintError h $ "No such variable " ++ show n
255− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
256+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
256 putIState ist
257 putIState ist
257− return (False, e, False, prf, Right ""))
258+ return (False, e, False, prf, Right action))
258 (\err -> do putIState ist ; ierror err)
259 (\err -> do putIState ist ; ierror err)
260 checkType t = do
261 checkType t = do
@@ -269,14 +270,14 @@ ploop fn d prompt prf e h
269 ty' = normaliseC ctxt [] ty
270 ty' = normaliseC ctxt [] ty
270 h = idris_outh ist
271 h = idris_outh ist
271 infixes = idris_infixes ist
272 infixes = idris_infixes ist
272− case tm of
273+ action = case tm of
273− TType _ ->
274+ TType _ ->
274− ihPrintTermWithType h (prettyImp ppo PType) type1Doc
275+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
275− _ -> let bnd = map (\x -> (fst x, False)) env in
276+ _ -> let bnd = map (\x -> (fst x, False)) env in
276− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
277+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
277− (pprintPTerm ppo bnd [] infixes (delab ist ty))
278+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
278 putIState ist
279 putIState ist
279− return (False, e, False, prf, Right ""))
280+ return (False, e, False, prf, Right action))
280 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
281 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
282 evalTerm t e = withErrorReflection $
283 evalTerm t e = withErrorReflection $
@@ -295,7 +296,7 @@ ploop fn d prompt prf e h
295 infixes = idris_infixes ist
296 infixes = idris_infixes ist
296 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
297 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
297 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
298 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
298− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
299+ action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
299 putIState ist
300 putIState ist
300− return (False, e, False, prf, Right ""))
301+ return (False, e, False, prf, Right action))
301 (\err -> do putIState ist ; ierror err)
302 (\err -> do putIState ist ; ierror err)