2f93ad9 · Idris-dev · git.iko.soy

204 case cmd of

205 Success Abandon -> do iPrintError ""; ifail "Abandoned"

206 _ -> return ()

207− (d, st, done, prf') <- idrisCatch

207+ (d, st, done, prf', res) <- idrisCatch

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

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

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

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

211+ return (True, st, False, init prf, Right "")

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

212+ Success ProofState -> return (True, e, False, prf, Right "")

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

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

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

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

216− return (False, e, False, prf)

215+ return (False, e, False, prf, Right "")

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

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

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

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

219 iputStrLn "Proof completed!"

218 iputStrLn "Proof completed!"

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

219+ return (False, e, True, prf, Right "")

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

220+ Success (TCheck (PRef _ n)) -> checkNameType 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) ->

221+ Success (TCheck t) -> checkType 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 $

222+ Success (TEval t) -> evalTerm t e

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)

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

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

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

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

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

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

225+ return (True, st, False, prf ++ [step], Right ""))

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

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

226+ (\err -> return (False, e, False, prf, Left err))

287 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 ->

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

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

289− return (tm, prf')

233+ return (tm, prf')

290− else do iPrintResult ""

234+ else do iPrintResult ok

291− ploop fn d prompt prf' st h'

235+ ploop fn d prompt prf' st h'

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