c29e746 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow :doc in prover

This supports looking up documentation while proving. It's really most useful inside of an IDE.

commitc29e746296fa498228a8812ecbbea108b6e09081 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 10 Jul 2014, 00:39 (12 years ago) parent3a2c8aa

3 files changed+29

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/ParseExpr.hs+10 src/Idris/Prover.hs+18

src/Idris/AbsSyntaxTree.hs+1

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

761761 | GoalType String (PTactic' t)

762762 | TCheck t

763763 | TEval t

764+ | TDocStr (Either Name Const)

764765 | Qed | Abandon

765766 deriving (Show, Eq, Functor)

766767{-!

src/Idris/ParseExpr.hs+10

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

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

12861286 i <- get

12871287 return $ TCheck (desugar syn i t))

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

1289+ whiteSpace

1290+ c <- constant

1291+ eof

1292+ return (TDocStr (Right c)))

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

1294+ whiteSpace

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

1296+ eof

1297+ return (TDocStr (Left n)))

12881298 <?> "prover command")

12891299 <?> "tactic"

12901300 where

src/Idris/Prover.hs+18

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

99import Idris.AbsSyntax

1010import Idris.AbsSyntaxTree

1111import Idris.Delaborate

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

1213import Idris.ElabDecls

1314import Idris.ElabTerm

1415import Idris.Parser hiding (params)

@@ -181,6 +182,7 @@ receiveInput e =

181182 receiveInput e

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

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

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

184186 _ -> return Nothing

185187

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

@@ -224,6 +226,7 @@ ploop fn d prompt prf e h

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

225227 Success (TCheck t) -> checkType t

226228 Success (TEval t) -> evalTerm t e

229+ Success (TDocStr x) -> docStr x

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

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

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

@@ -300,3 +303,18 @@ ploop fn d prompt prf e h

300303 putIState ist

301304 return (False, e, False, prf, Right action))

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