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

idris.cabal+4

compare with master

unifiedsplit

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

422 test/idrisdoc008/expected

423 test/idrisdoc008/*.idr

424 test/idrisdoc008/*.ipkg

425+ test/idrisdoc009/run

426+ test/idrisdoc009/expected

427+ test/idrisdoc009/*.idr

428+

425

429

426 test/interactive001/run

430 test/interactive001/run

427 test/interactive001/input

431 test/interactive001/input

src/Idris/AbsSyntaxTree.hs+12−1

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

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

167 idris_calledgraph :: Ctxt [Name],

168 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

169 idris_tyinfodata :: Ctxt TIData,

172 idris_tyinfodata :: Ctxt TIData,

170 idris_fninfo :: Ctxt FnInfo,

173 idris_fninfo :: Ctxt FnInfo,

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

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

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

285 | IBCPostulate Name

288 | IBCPostulate Name

286 | IBCTotCheckErr FC String

289 | IBCTotCheckErr FC String

287 | IBCParsedRegion FC

290 | IBCParsedRegion FC

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

288 deriving Show

292 deriving Show

289

293

290-- | The initial state for the compiler

294-- | The initial state for the compiler

291idrisInit :: IState

295idrisInit :: IState

296+idrisInit = IState initContext [] []

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

297+ emptyContext emptyContext emptyContext emptyContext

293 emptyContext emptyContext emptyContext emptyContext

298 emptyContext emptyContext emptyContext emptyContext

294 emptyContext emptyContext emptyContext emptyContext

299 emptyContext emptyContext emptyContext emptyContext

295 emptyContext emptyContext emptyContext emptyContext

300 emptyContext emptyContext emptyContext emptyContext

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

1197

1202

1198eqOpts = []

1203eqOpts = []

1199

1204

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+

1200-- Defined in builtins.idr

1211-- Defined in builtins.idr

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

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

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

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

src/Idris/Chaser.hs+1−1

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

135 if exist then do

136 file_in <- runIO $ readFile f

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

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

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

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

140 clearParserWarnings

141 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 #-}

2

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

4module Idris.Core.Binary where

src/Idris/Docs.hs+14

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

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

32 [PTerm] -- instances

33 [PTerm] -- superclasses

34+ | ModDoc [String] -- Module name

35+ (Docstring DocTerm)

34

36

35showDoc ist d

37showDoc ist d

36 | nullDocstring d = empty

38 | nullDocstring d = empty

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

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

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

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

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

140

142

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

141getDocs :: Name -> Idris Docs

149getDocs :: 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."

142getDocs n

156getDocs n

143 = do i <- getIState

157 = do i <- getIState

144 case lookupCtxt n (idris_classes i) of

158 case lookupCtxt n (idris_classes i) of

src/Idris/IBC.hs+17−5

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

35import Util.Zlib (decompressEither)

36

37ibcVersion :: Word8

38−ibcVersion = 90

38+ibcVersion = 92

39

40data IBCFile = IBCFile { ver :: Word8,

41 sourcefile :: FilePath,

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

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

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

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

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

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

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

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

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

70 ibc_coercions :: ![Name],

71 ibc_coercions :: ![Name],

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

84!-}

85!-}

85

86

86initIBC :: IBCFile

87initIBC :: IBCFile

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

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

88

89

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

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

90 -> FilePath -> Idris ()

91 -> FilePath -> Idris ()

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

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

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

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

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

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

283ibc 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"

283

287

284process :: Bool -- ^ Reexporting

288process :: Bool -- ^ Reexporting

285 -> IBCFile -> FilePath -> Idris ()

289 -> IBCFile -> FilePath -> Idris ()

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

324 pTotCheckErr $ force (ibc_totcheckfail i)

328 pTotCheckErr $ force (ibc_totcheckfail i)

325 pCG $ force (ibc_cg i)

329 pCG $ force (ibc_cg i)

326 pDocs $ force (ibc_docstrings i)

330 pDocs $ force (ibc_docstrings i)

331+ pMDocs $ force (ibc_moduledocs i)

327 pCoercions $ force (ibc_coercions i)

332 pCoercions $ force (ibc_coercions i)

328 pTrans $ force (ibc_transforms i)

333 pTrans $ force (ibc_transforms i)

329 pErrRev $ force (ibc_errRev i)

334 pErrRev $ force (ibc_errRev i)

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

502 update t = t

507 update t = t

503

508

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

509pDocs :: [(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) }

506

516

507pAccess :: Bool -- ^ Reexporting?

517pAccess :: Bool -- ^ Reexporting?

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

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

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

918 return (DataMI x1)

928 return (DataMI x1)

919

929

920instance Binary IBCFile where

930instance 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)

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

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

923 do put x1

933 do put x1

924 put x2

934 put x2

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

960 put x38

970 put x38

961 put x39

971 put x39

962 put x40

972 put x40

973+ put x41

963

974

964 get

975 get

965 = do x1 <- get

976 = do x1 <- get

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

1003 x38 <- get

1014 x38 <- get

1004 x39 <- get

1015 x39 <- get

1005 x40 <- get

1016 x40 <- get

1017+ x41 <- 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)

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)

1007 else return (initIBC { ver = x1 })

1019 else return (initIBC { ver = x1 })

1008

1020

1009instance Binary DataOpt where

1021instance Binary DataOpt where

src/Idris/Parser.hs+35−13

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

24import Idris.Imports

25import Idris.Delaborate

26import Idris.Error

27+import Idris.Elab.Value

27import Idris.ElabDecls

28import Idris.ElabDecls

28import Idris.ElabTerm

29import Idris.ElabTerm

29import Idris.Coverage

30import Idris.Coverage

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

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

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

91@

92@

92-}

93-}

93−moduleHeader :: IdrisParser [String]

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

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

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

96+ noArgs docs

95 reserved "module"

97 reserved "module"

96 i <- identifier

98 i <- identifier

97 option ';' (lchar ';')

99 option ';' (lchar ';')

98− return (moduleName i))

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

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

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

100− return [])

102+ return (Nothing, []))

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

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

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

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

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

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

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

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

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

108+ noArgs _ = return ()

105

109

106{- | Parses an import statement

110{- | Parses an import statement

107

111

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

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

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

1134

1138

1135-- | Parse module header and imports

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

1137parseImports fname input

1141parseImports fname input

1138 = do i <- getIState

1142 = do i <- getIState

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

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

1140 Failure err -> fail (show err)

1144 Failure err -> fail (show err)

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

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

1142 return x

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

1144 imports = do whiteSpace

1148 imports = do whiteSpace

1145− mname <- moduleHeader

1149+ (mdoc, mname) <- moduleHeader

1146− ps <- many import_

1150+ ps <- many import_

1147− mrk <- mark

1151+ mrk <- mark

1148− isEof <- lookAheadMatches eof

1152+ isEof <- lookAheadMatches eof

1149 let mrk' = if isEof

1153 let mrk' = if isEof

1150 then Nothing

1154 then Nothing

1151 else Just mrk

1155 else Just mrk

1152 i <- get

1156 i <- get

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

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

1154

1158

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

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

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

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

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

1261 let def_total = default_total i

1265 let def_total = default_total i

1262 file_in <- runIO $ readFile f

1266 file_in <- runIO $ readFile f

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

1267 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

1265 ai <- getAutoImports

1269 ai <- getAutoImports

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

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

1267 ids <- allImportDirs

1271 ids <- allImportDirs

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

1340 i <- getIState

1344 i <- getIState

1341 addHides (hide_list i)

1345 addHides (hide_list i)

1342

1346

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+

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

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

1344 ok <- noErrors

1355 ok <- noErrors

1345 when ok $

1356 when ok $

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

1364 PInstance _ _ _ _ _ _ _ _ -> r

1375 PInstance _ _ _ _ _ _ _ _ -> r

1365 _ -> x

1376 _ -> x

1366

1377

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+

1367{- | Adds names to hide list -}

1389{- | Adds names to hide list -}

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

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

1369addHides xs = do i <- getIState

1391addHides xs = do i <- getIState

src/Idris/REPL.hs+6−1

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

887

888process fn (DocStr (Left n))

889 = 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

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

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

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

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

893 iRenderResult (vsep toShow)

895 iRenderResult (vsep toShow)

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

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

895 return $ pprintDocs ist doc

897 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"

896

901

897process fn (DocStr (Right c))

902process fn (DocStr (Right c))

898 = do ist <- getIState

903 = 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.

4+

5+Constructors:

6+ MkTest : Test

7+

8+

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