5700be7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1296 from david-christiansen/ide-prover

5700be7David Christiansen12 years ago

src/Idris/Prover.hs+13−9

compare with master

unifiedsplit

@@ -63,9 +63,10 @@ prove opt ctxt lit n ty

63 ideslavePutSExp "start-proof-mode" n

64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

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 ()

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

@@ -203,16 +209,14 @@ ploop fn d prompt prf e h

203 Failure err -> do iPrintError (show err)

209 Failure err -> do iPrintError (show err)

204 return (False, e, False, prf)

210 return (False, e, False, prf)

205 Success Undo -> do (_, st) <- elabStep e loadState

211 Success Undo -> do (_, st) <- elabStep e loadState

206− iPrintResult ""

207 return (True, st, False, init prf)

212 return (True, st, False, init prf)

208− Success ProofState -> do iPrintResult ""

209− return (True, e, False, prf)

213+ Success ProofState -> return (True, e, False, prf)

210 Success ProofTerm -> do tm <- lifte e get_term

214 Success ProofTerm -> do tm <- lifte e get_term

211− iPrintResult $ "TT: " ++ show tm ++ "\n"

215+ iputStrLn $ "TT: " ++ show tm ++ "\n"

212 return (False, e, False, prf)

216 return (False, e, False, prf)

213 Success Qed -> do hs <- lifte e get_holes

217 Success Qed -> do hs <- lifte e get_holes

214 when (not (null hs)) $ ifail "Incomplete proof"

218 when (not (null hs)) $ ifail "Incomplete proof"

215− iPrintResult "Proof completed!"

219+ iputStrLn "Proof completed!"

216 return (False, e, True, prf)

220 return (False, e, True, prf)

217 Success (TCheck (PRef _ n)) ->

221 Success (TCheck (PRef _ n)) ->

218 do ctxt <- getContext

222 do ctxt <- getContext

@@ -277,12 +281,12 @@ ploop fn d prompt prf e h

277 Success tac -> do (_, e) <- elabStep e saveState

281 Success tac -> do (_, e) <- elabStep e saveState

278 (_, st) <- elabStep e (runTac autoSolve i fn tac)

282 (_, st) <- elabStep e (runTac autoSolve i fn tac)

279-- trace (show (problems (proof st))) $

283-- trace (show (problems (proof st))) $

280− iPrintResult ""

281 return (True, st, False, prf ++ [step]))

284 return (True, st, False, prf ++ [step]))

282 (\err -> do iPrintError (pshow i err)

285 (\err -> do iPrintError (pshow i err)

283 return (False, e, False, prf))

286 return (False, e, False, prf))

284 ideslavePutSExp "write-proof-state" (prf', length prf')

287 ideslavePutSExp "write-proof-state" (prf', length prf')

285 if done then do (tm, _) <- elabStep st get_term

288 if done then do (tm, _) <- elabStep st get_term

286 return (tm, prf')

289 return (tm, prf')

290+ else do iPrintResult ""

287− else ploop fn d prompt prf' st h'

291+ ploop fn d prompt prf' st h'

288 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

292 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

src/Idris/REPL.hs+19−5

@@ -240,11 +240,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

240 i <- getIState

241 case parseCmd i "(input)" cmd of

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)