git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
9815da8Edwin Brady
src/Idris/Prover.hs+92−82
compare with master
unifiedsplit
@@ -63,9 +63,10 @@ prove opt ctxt lit n ty
63 ideslavePutSExp "start-proof-mode" n
63 ideslavePutSExp "start-proof-mode" n
64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
65 iLOG $ "Adding " ++ show tm
65 iLOG $ "Adding " ++ show tm
66− iputStrLn $ showProof lit n prf
67 i <- getIState
66 i <- getIState
67+ case idris_outputmode i of
68− ideslavePutSExp "end-proof-mode" n
68+ IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)
69+ _ -> iputStrLn $ showProof lit n prf
69 let proofs = proof_list i
70 let proofs = proof_list i
70 putIState (i { proof_list = (n, prf) : proofs })
71 putIState (i { proof_list = (n, prf) : proofs })
71 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
72 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
@@ -85,6 +86,11 @@ prove opt ctxt lit n ty
85 [([], P Ref n ty, ptm)]
86 [([], P Ref n ty, ptm)]
86 [([], P Ref n ty, ptm')] ty)
87 [([], P Ref n ty, ptm')] ty)
87 solveDeferred n
88 solveDeferred n
89+ case idris_outputmode i of
90+ IdeSlave n ->
91+ runIO . putStrLn $
92+ convSExp "return" (SymbolAtom "ok", "") n
93+ _ -> return ()
88
94
89elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
95elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
90elabStep st e = case runStateT eCheck st of
96elabStep st e = case runStateT eCheck st of
@@ -171,7 +177,7 @@ receiveInput e =
171 ideslavePutSExp "return" good
177 ideslavePutSExp "return" good
172 receiveInput e
178 receiveInput e
173 Just (Interpret cmd) -> return (Just cmd)
179 Just (Interpret cmd) -> return (Just cmd)
174− Nothing -> return Nothing
180+ _ -> return Nothing
175
181
176ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
182ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
177ploop fn d prompt prf e h
183ploop fn d prompt prf e h
@@ -198,91 +204,95 @@ ploop fn d prompt prf e h
198 case cmd of
204 case cmd of
199 Success Abandon -> do iPrintError ""; ifail "Abandoned"
205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
200 _ -> return ()
206 _ -> return ()
201− (d, st, done, prf') <- idrisCatch
207+ (d, st, done, prf', res) <- idrisCatch
202 (case cmd of
208 (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)
205 Success Undo -> do (_, st) <- elabStep e loadState
210 Success Undo -> do (_, st) <- elabStep e loadState
206− iPrintResult ""
207− return (True, st, False, init prf)
211+ return (True, st, False, init prf, Right "")
208− Success ProofState -> do iPrintResult ""
209− return (True, e, False, prf)
212+ Success ProofState -> return (True, e, False, prf, Right "")
210 Success ProofTerm -> do tm <- lifte e get_term
213 Success ProofTerm -> do tm <- lifte e get_term
211− iPrintResult $ "TT: " ++ show tm ++ "\n"
214+ iputStrLn $ "TT: " ++ show tm ++ "\n"
212− return (False, e, False, prf)
215+ return (False, e, False, prf, Right "")
213 Success Qed -> do hs <- lifte e get_holes
216 Success Qed -> do hs <- lifte e get_holes
214 when (not (null hs)) $ ifail "Incomplete proof"
217 when (not (null hs)) $ ifail "Incomplete proof"
215− iPrintResult "Proof completed!"
218+ iputStrLn "Proof completed!"
216− return (False, e, True, prf)
219+ return (False, e, True, prf, Right "")
217− Success (TCheck (PRef _ n)) ->
220+ Success (TCheck (PRef _ n)) -> checkNameType 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) ->
221+ Success (TCheck t) -> checkType 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 $
222+ Success (TEval t) -> evalTerm t e
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)
277 Success tac -> do (_, e) <- elabStep e saveState
223 Success tac -> do (_, e) <- elabStep e saveState
278 (_, st) <- elabStep e (runTac autoSolve i fn tac)
224 (_, st) <- elabStep e (runTac autoSolve i fn tac)
279−-- trace (show (problems (proof st))) $
280− iPrintResult ""
281− return (True, st, False, prf ++ [step]))
225+ return (True, st, False, prf ++ [step], Right ""))
282− (\err -> do iPrintError (pshow i err)
283− return (False, e, False, prf))
226+ (\err -> return (False, e, False, prf, Left err))
284 ideslavePutSExp "write-proof-state" (prf', length prf')
227 ideslavePutSExp "write-proof-state" (prf', length prf')
228+ case res of
229+ Left err -> do iPrintError (pshow i err)
230+ ploop fn d prompt prf' st h'
231+ Right ok ->
285− if done then do (tm, _) <- elabStep st get_term
232+ if done then do (tm, _) <- elabStep st get_term
286− return (tm, prf')
233+ return (tm, prf')
234+ else do iPrintResult ok
287− else ploop fn d prompt prf' st h'
235+ ploop fn d prompt prf' st h'
288 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
236 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)
src/Idris/REPL.hs+19−5
@@ -240,11 +240,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
240 i <- getIState
240 i <- getIState
241 case parseCmd i "(input)" cmd of
241 case parseCmd i "(input)" cmd of
242 Failure err -> iPrintError $ show (fixColour c err)
242 Failure err -> iPrintError $ show (fixColour c err)
243− Success (Prove n') -> do iPrintResult ""
243+ Success (Prove n') ->
244− idrisCatch
244+ idrisCatch
245− (process stdout fn (Prove n'))
245+ (do process stdout fn (Prove n')
246+ isetPrompt (mkPrompt mods)
247+ case idris_outputmode i of
248+ IdeSlave n -> -- signal completion of proof to ide
249+ runIO . hPutStrLn stdout $
250+ IdeSlave.convSExp "return"
251+ (IdeSlave.SymbolAtom "ok", "")
252+ n
253+ _ -> return ())
254+ (\e -> do ist <- getIState
255+ isetPrompt (mkPrompt mods)
256+ case idris_outputmode i of
257+ IdeSlave n ->
258+ runIO . hPutStrLn stdout $
259+ IdeSlave.convSExp "abandon-proof" "Abandoned" n
260+ _ -> return ()
246− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
261+ ihRenderError stdout $ pprintErr ist e)
247− isetPrompt (mkPrompt mods)
248 Success cmd -> idrisCatch
262 Success cmd -> idrisCatch
249 (ideslaveProcess fn cmd)
263 (ideslaveProcess fn cmd)
250 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
264 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)