6340534 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1371 from david-christiansen/prover-output-color

6340534David Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -761,6 +761,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

761 | GoalType String (PTactic' t)

762 | TCheck t

763 | TEval t

764+ | TDocStr (Either Name Const)

764 | Qed | Abandon

765 | Qed | Abandon

765 deriving (Show, Eq, Functor)

766 deriving (Show, Eq, Functor)

766{-!

767{-!

src/Idris/ParseExpr.hs+10

@@ -1288,6 +1288,16 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1288 t <- (indentPropHolds gtProp *> expr syn);

1289 i <- get

1290 return $ TCheck (desugar syn i t))

1291+ <|> try (do reserved "doc"

1292+ whiteSpace

1293+ c <- constant

1294+ eof

1295+ return (TDocStr (Right c)))

1296+ <|> try (do reserved "doc"

1297+ whiteSpace

1298+ n <- (fnName <|> (string "_|_" >> return falseTy))

1299+ eof

1300+ return (TDocStr (Left n)))

1291 <?> "prover command")

1301 <?> "prover command")

1292 <?> "tactic"

1302 <?> "tactic"

1293 where

1303 where

src/Idris/Prover.hs+38−19

@@ -9,6 +9,7 @@ import Idris.Core.Typecheck

9import Idris.AbsSyntax

10import Idris.AbsSyntaxTree

11import Idris.Delaborate

12+import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)

12import Idris.ElabDecls

13import Idris.ElabDecls

13import Idris.ElabTerm

14import Idris.ElabTerm

14import Idris.Parser hiding (params)

15import Idris.Parser hiding (params)

@@ -180,6 +181,8 @@ receiveInput e =

180 ideslavePutSExp "return" good

181 ideslavePutSExp "return" good

181 receiveInput e

182 receiveInput e

182 Just (Interpret cmd) -> return (Just cmd)

183 Just (Interpret cmd) -> return (Just cmd)

184+ Just (TypeOf str) -> return (Just (":t " ++ str))

185+ Just (DocsFor str) -> return (Just (":doc " ++ str))

183 _ -> return Nothing

186 _ -> return Nothing

184

187

185ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

188ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

@@ -211,21 +214,22 @@ ploop fn d prompt prf e h

211 (case cmd of

214 (case cmd of

212 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

215 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

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

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

214− return (True, st, False, init prf, Right "")

217+ return (True, st, False, init prf, Right $ iPrintResult "")

215− Success ProofState -> return (True, e, False, prf, Right "")

218+ Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

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

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

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

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

218− return (False, e, False, prf, Right "")

221+ return (False, e, False, prf, Right $ iPrintResult "")

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

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

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

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

221 iputStrLn "Proof completed!"

224 iputStrLn "Proof completed!"

222− return (False, e, True, prf, Right "")

225+ return (False, e, True, prf, Right $ iPrintResult "")

223 Success (TCheck (PRef _ n)) -> checkNameType n

226 Success (TCheck (PRef _ n)) -> checkNameType n

224 Success (TCheck t) -> checkType t

227 Success (TCheck t) -> checkType t

225 Success (TEval t) -> evalTerm t e

228 Success (TEval t) -> evalTerm t e

229+ Success (TDocStr x) -> docStr x

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

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

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

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

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

232+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

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

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

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

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

231 case res of

235 case res of

@@ -234,7 +238,7 @@ ploop fn d prompt prf e h

234 Right ok ->

238 Right ok ->

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

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

236 return (tm, prf')

240 return (tm, prf')

237− else do iPrintResult ok

241+ else do ok

238 ploop fn d prompt prf' st h'

242 ploop fn d prompt prf' st h'

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

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

240 checkNameType n = do

244 checkNameType n = do

@@ -250,11 +254,11 @@ ploop fn d prompt prf e h

250 putIState ist'

254 putIState ist'

251 -- Unlike the REPL, metavars have no special treatment, to

255 -- Unlike the REPL, metavars have no special treatment, to

252 -- make it easier to see how to prove with them.

256 -- make it easier to see how to prove with them.

253− case lookupNames n ctxt' of

257+ let action = case lookupNames n ctxt' of

254− [] -> ihPrintError h $ "No such variable " ++ show n

258+ [] -> ihPrintError h $ "No such variable " ++ show n

255− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

259+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

256 putIState ist

260 putIState ist

257− return (False, e, False, prf, Right ""))

261+ return (False, e, False, prf, Right action))

258 (\err -> do putIState ist ; ierror err)

262 (\err -> do putIState ist ; ierror err)

259

263

260 checkType t = do

264 checkType t = do

@@ -269,14 +273,14 @@ ploop fn d prompt prf e h

269 ty' = normaliseC ctxt [] ty

273 ty' = normaliseC ctxt [] ty

270 h = idris_outh ist

274 h = idris_outh ist

271 infixes = idris_infixes ist

275 infixes = idris_infixes ist

272− case tm of

276+ action = case tm of

273− TType _ ->

277+ TType _ ->

274− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

278+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

275− _ -> let bnd = map (\x -> (fst x, False)) env in

279+ _ -> let bnd = map (\x -> (fst x, False)) env in

276− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

280+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

277− (pprintPTerm ppo bnd [] infixes (delab ist ty))

281+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

278 putIState ist

282 putIState ist

279− return (False, e, False, prf, Right ""))

283+ return (False, e, False, prf, Right action))

280 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

284 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

281

285

282 evalTerm t e = withErrorReflection $

286 evalTerm t e = withErrorReflection $

@@ -295,7 +299,22 @@ ploop fn d prompt prf e h

295 infixes = idris_infixes ist

299 infixes = idris_infixes ist

296 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

300 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

297 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

301 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

298− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

302+ action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

299 putIState ist

303 putIState ist

300− return (False, e, False, prf, Right ""))

304+ return (False, e, False, prf, Right action))

301 (\err -> do putIState ist ; ierror err)

305 (\err -> do putIState ist ; ierror err)

306+ docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))

307+ docStr (Left n) = do ist <- getIState

308+ let h = idris_outh ist

309+ idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

310+ [] -> return (False, e, False, prf,

311+ Left . Msg $ "No documentation for " ++ show n)

312+ ns -> do toShow <- mapM (showDoc ist) ns

313+ return (False, e, False, prf,

314+ Right $ ihRenderResult h (vsep toShow)))

315+ (\err -> do putIState ist ; ierror err)

316+ where showDoc ist (n, d) = do doc <- getDocs n

317+ return $ pprintDocs ist doc

318+ docStr (Right c) = do ist <- getIState

319+ let h = idris_outh ist

320+ return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))