ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1982 from david-christiansen/feature/ide-doc-overview

Browse Source 
Add the ability for IDEs to get documentation overviews
This commit is contained in:
David Christiansen 2015-03-06 18:02:27 +01:00
commit 49fffbcf5c
7 changed files with 67 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/AbsSyntaxTree.hs
View File

@ -336,6 +336,8 @@ data Codegen = Via String
deriving instance NFData Codegen
!-}
data HowMuchDocs = FullDocs | OverviewDocs
-- | REPL commands
data Command = Quit
| Help
@ -343,7 +345,7 @@ data Command = Quit
| NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
| Undefine [Name]
| Check PTerm
| DocStr (Either Name Const)
| DocStr (Either Name Const) HowMuchDocs
| TotCheck Name
| Reload
| Load FilePath (Maybe Int) -- up to maximum line number

66
src/Idris/Docs.hs
View File

@ -1,12 +1,12 @@
{-# LANGUAGE PatternGuards #-}
module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where
{-# LANGUAGE DeriveFunctor, PatternGuards #-}
module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Delaborate
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm)
import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)
import Util.Pretty
@ -18,21 +18,27 @@ import qualified Data.Text as T
--
-- Issue #1573 on the Issue tracker.
-- https://github.com/idris-lang/Idris-dev/issues/1573
data FunDoc = FD Name (Docstring DocTerm)
[(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] -- args: name, ty, implicit, docs
PTerm -- function type
(Maybe Fixity)
data FunDoc' d = FD Name d
[(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs
PTerm -- function type
(Maybe Fixity)
deriving Functor
data Docs = FunDoc FunDoc
| DataDoc FunDoc -- type constructor docs
[FunDoc] -- data constructor docs
| ClassDoc Name (Docstring DocTerm)-- class docs
[FunDoc] -- method docs
[(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings
[PTerm] -- instances
[PTerm] -- superclasses
| ModDoc [String] -- Module name
(Docstring DocTerm)
type FunDoc = FunDoc' (Docstring DocTerm)
data Docs' d = FunDoc (FunDoc' d)
| DataDoc (FunDoc' d) -- type constructor docs
[FunDoc' d] -- data constructor docs
| ClassDoc Name d -- class docs
[FunDoc' d] -- method docs
[(Name, Maybe d)] -- parameters and their docstrings
[PTerm] -- instances
[PTerm] -- superclasses
| ModDoc [String] -- Module name
d
deriving Functor
type Docs = Docs' (Docstring DocTerm)
showDoc ist d
| nullDocstring d = empty
@ -144,23 +150,29 @@ pprintDocs ist (ModDoc mod docs)
= nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
-- | Determine a truncation function depending how much docs the user
-- wants to see
howMuch FullDocs = id
howMuch OverviewDocs = overview
-- | Given a fully-qualified, disambiguated name, construct the
-- documentation object for it
getDocs :: Name -> Idris Docs
getDocs n@(NS n' ns) | n' == modDocName
getDocs :: Name -> HowMuchDocs -> Idris Docs
getDocs n@(NS n' ns) w | n' == modDocName
= do i <- getIState
case lookupCtxtExact n (idris_moduledocs i) of
Just doc -> return $ ModDoc (reverse (map T.unpack ns)) doc
Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
" do not exist! This shouldn't have happened and is a bug."
getDocs n
getDocs n w
= do i <- getIState
case lookupCtxt n (idris_classes i) of
[ci] -> docClass n ci
_ -> case lookupCtxt n (idris_datatypes i) of
[ti] -> docData n ti
_ -> do fd <- docFun n
return (FunDoc fd)
docs <- case lookupCtxt n (idris_classes i) of
[ci] -> docClass n ci
_ -> case lookupCtxt n (idris_datatypes i) of
[ti] -> docData n ti
_ -> do fd <- docFun n
return (FunDoc fd)
return $ fmap (howMuch w) docs
docData :: Name -> TypeInfo -> Idris Docs
docData n ti

11
src/Idris/IdeMode.hs
View File

@ -2,7 +2,7 @@
{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
module Idris.IdeMode(parseMessage, convSExp, IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where
module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where
import Text.Printf
import Numeric
@ -206,6 +206,8 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
data Opt = ShowImpl | ErrContext deriving Show
data WhatDocs = Overview | Full
data IdeModeCommand = REPLCompletions String
| Interpret String
| TypeOf String
@ -217,7 +219,7 @@ data IdeModeCommand = REPLCompletions String
| ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
| MakeLemma Int String
| LoadFile String (Maybe Int)
| DocsFor String
| DocsFor String WhatDocs
| Apropos String
| GetOpts
| SetOpt Opt Bool
@ -258,7 +260,10 @@ sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAt
_ -> Nothing)
sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)
sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])
| Just w <- lookup s opts = Just (DocsFor name w)
where opts = [("overview", Overview), ("full", Full)]
sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
sexpToCommand (SymbolAtom "get-options") = Just GetOpts
sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

2
src/Idris/IdrisDoc.hs
View File

@ -273,7 +273,7 @@ loadDocs :: IState -- ^ IState to extract infomation from
-> Name -- ^ Name to load Docs for
-> IO (Maybe Docs)
loadDocs ist n
| mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n) ist
| mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n FullDocs) ist
case docs of Right d -> return (Just d)
Left _ -> return Nothing
| otherwise = return Nothing

4
src/Idris/Prover.hs
View File

@ -202,7 +202,7 @@ receiveInput h e =
receiveInput h e
Just (IdeMode.Interpret cmd) -> return (Just cmd)
Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
Just (IdeMode.DocsFor str) -> return (Just (":doc " ++ str))
Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
_ -> return Nothing
ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
@ -336,7 +336,7 @@ ploop fn d prompt prf e h
return (False, e, False, prf,
Right $ iRenderResult (vsep toShow)))
(\err -> do putIState ist ; ierror err)
where showDoc ist (n, d) = do doc <- getDocs n
where showDoc ist (n, d) = do doc <- getDocs n FullDocs
return $ pprintDocs ist doc
docStr (Right c) = do ist <- getIState
return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

20
src/Idris/REPL.hs
View File

@ -344,13 +344,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =
Left err -> iPrintError err
Right n -> process "(idemode)"
(Check (PRef (FC "(idemode)" (0,0) (0,0)) n))
runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =
runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =
case parseConst orig name of
Success c -> process "(idemode)" (DocStr (Right c))
Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))
Failure _ ->
case splitName name of
Left err -> iPrintError err
Right n -> process "(idemode)" (DocStr (Left n))
Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))
where howMuch IdeMode.Overview = OverviewDocs
howMuch IdeMode.Full = FullDocs
runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =
process fn (CaseSplitAt False line (sUN name))
runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =
@ -553,7 +555,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)
idemodeProcess fn (ExecVal t) = process fn (ExecVal t)
idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
idemodeProcess fn (Check t) = process fn (Check t)
idemodeProcess fn (DocStr n) = process fn (DocStr n)
idemodeProcess fn (DocStr n w) = process fn (DocStr n w)
idemodeProcess fn Universes = process fn Universes
idemodeProcess fn (Defn n) = do process fn (Defn n)
iPrintResult ""
@ -905,21 +907,23 @@ process fn (Check t)
_ -> iPrintTermWithType (pprintDelab ist tm)
(pprintDelab ist ty)
process fn (DocStr (Left n))
process fn (DocStr (Left n) w)
= do ist <- getIState
let docs = lookupCtxtName n (idris_docstrings ist) ++
map (\(n,d)-> (n, (d,[]))) (lookupCtxtName (modDocN n) (idris_moduledocs ist))
map (\(n,d)-> (n, (d, [])))
(lookupCtxtName (modDocN n) (idris_moduledocs ist))
case docs of
[] -> iPrintError $ "No documentation for " ++ show n
ns -> do toShow <- mapM (showDoc ist) ns
iRenderResult (vsep toShow)
where showDoc ist (n, d) = do doc <- getDocs n
where showDoc ist (n, d) = do doc <- getDocs n w
return $ pprintDocs ist doc
modDocN (NS (UN n) ns) = NS modDocName (n:ns)
modDocN (UN n) = NS modDocName [n]
modDocN _ = sMN 1 "NotFoundForSure"
process fn (DocStr (Right c))
process fn (DocStr (Right c) _) -- constants only have overviews
= do ist <- getIState
iRenderResult $ pprintConstDocs ist c (constDocs c)

4
src/Idris/REPLParser.hs
View File

@ -258,9 +258,9 @@ cmd_doc name = do
let constant = do
c <- P.constant
eof
return $ Right (DocStr (Right c))
return $ Right (DocStr (Right c) FullDocs)
let fnName = fnNameArg (\n -> DocStr (Left n)) name
let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name
try constant <|> fnName