0b3b0b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Display useful information on :doc

0b3b0b5Edwin Brady14 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -76,7 +76,7 @@ Executable idris

76 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

77 Idris.Coverage, Idris.IBC, Idris.Unlit,

78 Idris.DataOpts, Idris.Transforms, Idris.DSL,

79− Idris.UnusedArgs,

79+ Idris.UnusedArgs, Idris.Docs,

81 Util.Pretty, Util.System,

82 Pkg.Package, Pkg.PParser,

src/Idris/Docs.hsnew file+97

@@ -0,0 +1,97 @@

1+module Idris.Docs where

3+import Idris.AbsSyntax

4+import Idris.Delaborate

5+import Core.TT

6+import Core.Evaluate

8+import Data.Maybe

10+data FunDoc = Doc Name String

11+ [(Name, PArg)] -- args

12+ PTerm -- function type

13+

14+data Doc = FunDoc FunDoc

15+ | DataDoc FunDoc -- type constructor docs

16+ [FunDoc] -- data constructor docs

17+ | ClassDoc Name String -- class docs

18+ [FunDoc] -- method docs

19+

20+showDoc "" = ""

21+showDoc x = " -- " ++ x ++ "\n"

22+

23+instance Show FunDoc where

24+ show (Doc n doc args ty)

25+ = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++

26+ let argshow = mapMaybe showArg args in

27+ if (not (null argshow)) then "Arguments:\n\t" ++

28+ showSep "\t" argshow

29+ else ""

30+ where showArg (n, arg@(PExp _ _ _ _))

31+ = Just $ showName n ++ show (getTm arg) ++

32+ showDoc (pargdoc arg) ++ "\n"

33+ showArg (n, arg@(PConstraint _ _ _ _))

34+ = Just $ "Class constraint " ++

35+ show (getTm arg) ++ showDoc (pargdoc arg)

36+ ++ "\n"

37+ showArg (n, arg@(PImp _ _ _ _ doc))

38+ | not (null doc)

39+ = Just $ "(implicit) " ++

40+ show n ++ " : " ++ show (getTm arg)

41+ ++ showDoc (pargdoc arg) ++ "\n"

42+ showArg (n, _) = Nothing

43+

44+ showName (MN _ _) = ""

45+ showName x = show x ++ " : "

46+

47+instance Show Doc where

48+

49+ show (FunDoc d) = show d

50+ show (DataDoc t args) = "Data type " ++ show t ++

51+ "\nConstructors:\n\n" ++

52+ showSep "\n" (map show args)

53+ show (ClassDoc n doc meths)

54+ = "Type class " ++ show n ++ -- parameters?

55+ "\nMethods:\n\n" ++

56+ showSep "\n" (map show meths)

57+

58+getDocs :: Name -> Idris Doc

59+getDocs n

60+ = do i <- getIState

61+ case lookupCtxt Nothing n (idris_classes i) of

62+ [ci] -> docClass n ci

63+ _ -> case lookupCtxt Nothing n (idris_datatypes i) of

64+ [ti] -> docData n ti

65+ _ -> do fd <- docFun n

66+ return (FunDoc fd)

67+

68+docData :: Name -> TypeInfo -> Idris Doc

69+docData n ti

70+ = do tdoc <- docFun n

71+ cdocs <- mapM docFun (con_names ti)

72+ return (DataDoc tdoc cdocs)

73+

74+docClass :: Name -> ClassInfo -> Idris Doc

75+docClass n ci

76+ = do i <- getIState

77+ let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

78+ [str] -> str

79+ _ -> ""

80+ mdocs <- mapM docFun (map fst (class_methods ci))

81+ return (ClassDoc n docstr mdocs)

82+

83+docFun :: Name -> Idris FunDoc

84+docFun n

85+ = do i <- getIState

86+ let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

87+ [str] -> str

88+ _ -> ""

89+ let ty = case lookupTy Nothing n (tt_ctxt i) of

90+ (t : _) -> t

91+ let argnames = map fst (getArgTys ty)

92+ let args = case lookupCtxt Nothing n (idris_implicits i) of

93+ [args] -> zip argnames args

94+ _ -> []

95+ return (Doc n docstr args (delab i ty))

96+

97+

src/Idris/ElabDecls.hs+1−1

@@ -80,7 +80,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

81elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

82elabData info syn doc fc codata (PLaterdecl n t_in)

83− = do iLOG (show fc)

83+ = do iLOG (show (fc, doc))

84 checkUndefined fc n

85 ctxt <- getContext

86 i <- get

src/Idris/REPL.hs+5−2

@@ -15,6 +15,7 @@ import Idris.Parser

15import Idris.Primitives

16import Idris.Coverage

17import Idris.UnusedArgs

18+import Idris.Docs

19import Paths_idris

20import Paths_idris

20import Util.System

21import Util.System

@@ -199,9 +200,11 @@ process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

199

200

200process fn (DocStr n) = do i <- get

201process fn (DocStr n) = do i <- get

201 case lookupCtxtName Nothing n (idris_docstrings i) of

202 case lookupCtxtName Nothing n (idris_docstrings i) of

202− [] -> iputStrLn "No documentation"

203+ [] -> iputStrLn $ "No documentation for " ++ show n

203 ns -> mapM_ showDoc ns

204 ns -> mapM_ showDoc ns

204− where showDoc (n, d) = iputStrLn $ show n ++ " : " ++ d

205+ where showDoc (n, d)

206+ = do doc <- getDocs n

207+ iputStrLn $ show doc

205process fn Universes = do i <- get

208process fn Universes = do i <- get

206 let cs = idris_constraints i

209 let cs = idris_constraints i

207-- iputStrLn $ showSep "\n" (map show cs)

210-- iputStrLn $ showSep "\n" (map show cs)