c29e746 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow :doc in prover

c29e746David Raymond 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

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

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

1286 i <- get

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

1288 <?> "prover command")

1298 <?> "prover command")

1289 <?> "tactic"

1299 <?> "tactic"

1290 where

1300 where

src/Idris/Prover.hs+18

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

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

181 receiveInput e

182 receiveInput e

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

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

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

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

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

184 _ -> return Nothing

186 _ -> return Nothing

185

187

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

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

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

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

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

225 Success (TCheck t) -> checkType t

227 Success (TCheck t) -> checkType t

226 Success (TEval t) -> evalTerm t e

228 Success (TEval t) -> evalTerm t e

229+ Success (TDocStr x) -> docStr x

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

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

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

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

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

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

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

300 putIState ist

303 putIState ist

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

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

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