6b803b7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow documentation for modules

The syntax is the same as for other documentation, right before the "module" declaration. For an example, see the "idrisdoc009" test. Terms in module documentation are elaborated in a context including all of its imports and definitions, so the documentation can provide examples and descriptions. The :doc command now also shows documentation for modules.

commit6b803b7b63d9b4aef30cd2270c661c0ecbf3cf70 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 3 Jan 2015, 18:27 (12 years ago) parentc1cf03f

12 files changed+168−22

compare with master

unifiedsplit

idris.cabal+4 src/Idris/AbsSyntaxTree.hs+12−1 src/Idris/Chaser.hs+1−1 src/Idris/Core/Binary.hs+1−1 src/Idris/Docs.hs+14 src/Idris/IBC.hs+17−5 src/Idris/Parser.hs+35−13 src/Idris/REPL.hs+6−1 test/idrisdoc009/Test.idr+45 test/idrisdoc009/expected+29 test/idrisdoc009/input+1 test/idrisdoc009/run+3

idris.cabal+4

@@ -422,6 +422,10 @@ Extra-source-files:

422422 test/idrisdoc008/expected

423423 test/idrisdoc008/*.idr

424424 test/idrisdoc008/*.ipkg

425+ test/idrisdoc009/run

426+ test/idrisdoc009/expected

427+ test/idrisdoc009/*.idr

428+

425429

426430 test/interactive001/run

427431 test/interactive001/input

src/Idris/AbsSyntaxTree.hs+12−1

@@ -166,6 +166,9 @@ data IState = IState {

166166 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

167167 idris_calledgraph :: Ctxt [Name],

168168 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),

169+ idris_moduledocs :: Ctxt (Docstring DocTerm),

170+ -- ^ module documentation is saved in a special MN so the context

171+ -- mechanism can be used for disambiguation

169172 idris_tyinfodata :: Ctxt TIData,

170173 idris_fninfo :: Ctxt FnInfo,

171174 idris_transforms :: Ctxt [(Term, Term)],

@@ -285,11 +288,13 @@ data IBCWrite = IBCFix FixDecl

285288 | IBCPostulate Name

286289 | IBCTotCheckErr FC String

287290 | IBCParsedRegion FC

291+ | IBCModDocs Name -- ^ The name is the special name used to track module docs

288292 deriving Show

289293

290294-- | The initial state for the compiler

291295idrisInit :: IState

292−idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

296+idrisInit = IState initContext [] []

297+ emptyContext emptyContext emptyContext emptyContext

293298 emptyContext emptyContext emptyContext emptyContext

294299 emptyContext emptyContext emptyContext emptyContext

295300 emptyContext emptyContext emptyContext emptyContext

@@ -1197,6 +1202,12 @@ eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pac

11971202

11981203eqOpts = []

11991204

1205+-- | The special name to be used in the module documentation context -

1206+-- not for use in the main definition context. The namespace around it

1207+-- will determine the module to which the docs adhere.

1208+modDocName :: Name

1209+modDocName = sMN 0 "ModuleDocs"

1210+

12001211-- Defined in builtins.idr

12011212sigmaTy = sNS (sUN "Sigma") ["Builtins"]

12021213existsCon = sNS (sUN "MkSigma") ["Builtins"]

src/Idris/Chaser.hs+1−1

@@ -135,7 +135,7 @@ buildTree built fp = btree [] fp

135135 if exist then do

136136 file_in <- runIO $ readFile f

137137 file <- if lit then tclift $ unlit f file_in else return file_in

138− (_, modules, _) <- parseImports f file

138+ (_, _, modules, _) <- parseImports f file

139139 -- The chaser should never report warnings from sub-modules

140140 clearParserWarnings

141141 ms <- mapM (btree done) [realName | (_, realName, alias, fc) <- modules]

src/Idris/Core/Binary.hs+1−1

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33{-| Binary instances for the core datatypes -}

44module Idris.Core.Binary where

src/Idris/Docs.hs+14

@@ -31,6 +31,8 @@ data Docs = FunDoc FunDoc

3131 [(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings

3232 [PTerm] -- instances

3333 [PTerm] -- superclasses

34+ | ModDoc [String] -- Module name

35+ (Docstring DocTerm)

3436

3537showDoc ist d

3638 | nullDocstring d = empty

@@ -138,7 +140,19 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

138140 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

139141 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

140142

143+pprintDocs ist (ModDoc mod docs)

144+ = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

145+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

146+

147+-- | Given a fully-qualified, disambiguated name, construct the

148+-- documentation object for it

141149getDocs :: Name -> Idris Docs

150+getDocs n@(NS n' ns) | n' == modDocName

151+ = do i <- getIState

152+ case lookupCtxtExact n (idris_moduledocs i) of

153+ Just doc -> return $ ModDoc (reverse (map T.unpack ns)) doc

154+ Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++

155+ " do not exist! This shouldn't have happened and is a bug."

142156getDocs n

143157 = do i <- getIState

144158 case lookupCtxt n (idris_classes i) of

src/Idris/IBC.hs+17−5

@@ -35,7 +35,7 @@ import Codec.Compression.Zlib (compress)

3535import Util.Zlib (decompressEither)

3636

3737ibcVersion :: Word8

38−ibcVersion = 90

38+ibcVersion = 92

3939

4040data IBCFile = IBCFile { ver :: Word8,

4141 sourcefile :: FilePath,

@@ -65,6 +65,7 @@ data IBCFile = IBCFile { ver :: Word8,

6565 ibc_cg :: ![(Name, CGInfo)],

6666 ibc_defs :: ![(Name, Def)],

6767 ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

68+ ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],

6869 ibc_transforms :: ![(Name, (Term, Term))],

6970 ibc_errRev :: ![(Term, Term)],

7071 ibc_coercions :: ![Name],

@@ -84,7 +85,7 @@ deriving instance Binary IBCFile

8485!-}

8586

8687initIBC :: IBCFile

87−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

88+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

8889

8990loadIBC :: Bool -- ^ True = reexport, False = make everything private

9091 -> FilePath -> Idris ()

@@ -280,6 +281,9 @@ ibc i (IBCMetavar n) f =

280281ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

281282ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

282283ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

284+ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

285+ Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

286+ _ -> ifail "IBC write failed"

283287

284288process :: Bool -- ^ Reexporting

285289 -> IBCFile -> FilePath -> Idris ()

@@ -324,6 +328,7 @@ process reexp i fn

324328 pTotCheckErr $ force (ibc_totcheckfail i)

325329 pCG $ force (ibc_cg i)

326330 pDocs $ force (ibc_docstrings i)

331+ pMDocs $ force (ibc_moduledocs i)

327332 pCoercions $ force (ibc_coercions i)

328333 pTrans $ force (ibc_transforms i)

329334 pErrRev $ force (ibc_errRev i)

@@ -502,7 +507,12 @@ pDefs reexp syms ds

502507 update t = t

503508

504509pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

505−pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

510+pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

511+

512+pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()

513+pMDocs ds = mapM_ addMDocStr ds

514+ where addMDocStr (n, d) = do ist <- getIState

515+ putIState ist { idris_moduledocs = addDef n d (idris_moduledocs ist) }

506516

507517pAccess :: Bool -- ^ Reexporting?

508518 -> [(Name, Accessibility)] -> Idris ()

@@ -918,7 +928,7 @@ instance Binary MetaInformation where

918928 return (DataMI x1)

919929

920930instance Binary IBCFile where

921− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40)

931+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41)

922932 = {-# SCC "putIBCFile" #-}

923933 do put x1

924934 put x2

@@ -960,6 +970,7 @@ instance Binary IBCFile where

960970 put x38

961971 put x39

962972 put x40

973+ put x41

963974

964975 get

965976 = do x1 <- get

@@ -1003,7 +1014,8 @@ instance Binary IBCFile where

10031014 x38 <- get

10041015 x39 <- get

10051016 x40 <- get

1006− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40)

1017+ x41 <- get

1018+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41)

10071019 else return (initIBC { ver = x1 })

10081020

10091021instance Binary DataOpt where

src/Idris/Parser.hs+35−13

@@ -24,6 +24,7 @@ import Idris.DSL

2424import Idris.Imports

2525import Idris.Delaborate

2626import Idris.Error

27+import Idris.Elab.Value

2728import Idris.ElabDecls

2829import Idris.ElabTerm

2930import Idris.Coverage

@@ -90,18 +91,21 @@ import System.IO

9091 ModuleHeader ::= 'module' Identifier_t ';'?;

9192@

9293-}

93−moduleHeader :: IdrisParser [String]

94−moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"

94+moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

95+moduleHeader = try (do docs <- optional docComment

96+ noArgs docs

9597 reserved "module"

9698 i <- identifier

9799 option ';' (lchar ';')

98− return (moduleName i))

100+ return (fmap fst docs, moduleName i))

99101 <|> try (do lchar '%'; reserved "unqualified"

100− return [])

101− <|> return (moduleName "Main")

102+ return (Nothing, []))

103+ <|> return (Nothing, moduleName "Main")

102104 where moduleName x = case span (/='.') x of

103105 (x, "") -> [x]

104106 (x, '.':y) -> x : moduleName y

107+ noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments"

108+ noArgs _ = return ()

105109

106110{- | Parses an import statement

107111

@@ -1133,24 +1137,24 @@ parseTactic :: IState -> String -> Result PTactic

11331137parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

11341138

11351139-- | Parse module header and imports

1136−parseImports :: FilePath -> String -> Idris ([String], [(Bool, String, Maybe String, FC)], Maybe Delta)

1140+parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta)

11371141parseImports fname input

11381142 = do i <- getIState

11391143 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

11401144 Failure err -> fail (show err)

11411145 Success (x, i) -> do putIState i

11421146 return x

1143− where imports :: IdrisParser (([String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)

1147+ where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState)

11441148 imports = do whiteSpace

1145− mname <- moduleHeader

1146− ps <- many import_

1147− mrk <- mark

1148− isEof <- lookAheadMatches eof

1149+ (mdoc, mname) <- moduleHeader

1150+ ps <- many import_

1151+ mrk <- mark

1152+ isEof <- lookAheadMatches eof

11491153 let mrk' = if isEof

11501154 then Nothing

11511155 else Just mrk

11521156 i <- get

1153− return ((mname, ps, mrk'), i)

1157+ return ((mdoc, mname, ps, mrk'), i)

11541158

11551159-- | There should be a better way of doing this...

11561160findFC :: Doc -> (FC, String)

@@ -1261,7 +1265,7 @@ loadSource lidr f toline

12611265 let def_total = default_total i

12621266 file_in <- runIO $ readFile f

12631267 file <- if lidr then tclift $ unlit f file_in else return file_in

1264− (mname, imports_in, pos) <- parseImports f file

1268+ (mdocs, mname, imports_in, pos) <- parseImports f file

12651269 ai <- getAutoImports

12661270 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in

12671271 ids <- allImportDirs

@@ -1340,6 +1344,13 @@ loadSource lidr f toline

13401344 i <- getIState

13411345 addHides (hide_list i)

13421346

1347+ -- Save module documentation if applicable

1348+ i <- getIState

1349+ case mdocs of

1350+ Nothing -> return ()

1351+ Just docs -> addModDoc syntax mname docs

1352+

1353+

13431354 -- Finally, write an ibc if checking was successful

13441355 ok <- noErrors

13451356 when ok $

@@ -1364,6 +1375,17 @@ loadSource lidr f toline

13641375 PInstance _ _ _ _ _ _ _ _ -> r

13651376 _ -> x

13661377

1378+ addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

1379+ addModDoc syn mname docs =

1380+ do ist <- getIState

1381+ docs' <- elabDocTerms recinfo (parsedDocs ist)

1382+ let modDocs' = addDef docName docs' (idris_moduledocs ist)

1383+ putIState ist { idris_moduledocs = modDocs' }

1384+ addIBC (IBCModDocs docName)

1385+ where

1386+ docName = NS modDocName (map T.pack (reverse mname))

1387+ parsedDocs ist = annotCode (tryFullExpr syn ist) docs

1388+

13671389{- | Adds names to hide list -}

13681390addHides :: [(Name, Maybe Accessibility)] -> Idris ()

13691391addHides xs = do i <- getIState

src/Idris/REPL.hs+6−1

@@ -887,12 +887,17 @@ process fn (Check t)

887887

888888process fn (DocStr (Left n))

889889 = do ist <- getIState

890− case lookupCtxtName n (idris_docstrings ist) of

890+ let docs = lookupCtxtName n (idris_docstrings ist) ++

891+ map (\(n,d)-> (n, (d,[]))) (lookupCtxtName (modDocN n) (idris_moduledocs ist))

892+ case docs of

891893 [] -> iPrintError $ "No documentation for " ++ show n

892894 ns -> do toShow <- mapM (showDoc ist) ns

893895 iRenderResult (vsep toShow)

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

895897 return $ pprintDocs ist doc

898+ modDocN (NS (UN n) ns) = NS modDocName (n:ns)

899+ modDocN (UN n) = NS modDocName [n]

900+ modDocN _ = sMN 1 "NotFoundForSure"

896901

897902process fn (DocStr (Right c))

898903 = do ist <- getIState

test/idrisdoc009/Test.idrnew file+45

@@ -0,0 +1,45 @@

1+||| Docs for module Test.

2+|||

3+||| It is a great module.

4+||| Prelude thingy:

5+||| ```idris example

6+||| "foo" ++ "bar"

7+||| ```

8+|||

9+||| Imported thingy:

10+||| ```idris example

11+||| 0.0 :+ 0.2

12+||| ```

13+|||

14+||| Type error:

15+||| ```idris

16+||| "foo" + 2

17+||| ```

18+|||

19+||| From this module:

20+||| ```idris example

21+||| MkTest

22+||| ```

23+module Test

24+import Data.Complex

25+

26+myplus : Nat -> Nat -> Nat

27+myplus Z j = j

28+myplus (S k) j = S (myplus k j)

29+

30+||| Docs for datatype Test.

31+data Test = MkTest

32+

33+data Thing : Type -> Type where

34+ MkThing : Thing Nat

35+

36+-- fnord ++ xyz do done let module argh

37+

38+namespace Main

39+ ||| Main is handy to do things in. ++.

40+ main : IO ()

41+ main = do putStrLn "Hi!"

42+ l <- getLine

43+ case l of

44+ "" => putStrLn "No!"

45+ str => putStrLn str

test/idrisdoc009/expectednew file+29

@@ -0,0 +1,29 @@

1+Type checking ./Test.idr

2+Data type Test : Type

3+ Docs for datatype Test.

5+Constructors:

6+ MkTest : Test

9+Module Test:

10+ Docs for module Test.

11+

12+ It is a great module. Prelude thingy:

13+

14+ > "foo" ++ "bar"

15+ "foobar"

16+

17+ Imported thingy:

18+

19+ > 0.0 :+ 0.2

20+ 0.0 :+ 0.2

21+

22+ Type error:

23+

24+ "foo" + 2

25+

26+ From this module:

27+

28+ > MkTest

29+ MkTest

test/idrisdoc009/inputnew file+1

@@ -0,0 +1 @@

1+:doc Test

test/idrisdoc009/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour --quiet Test.idr < input

3+rm -f *.ibc