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

CHANGELOG+1−1

compare with master

unifiedsplit

@@ -15,9 +15,9 @@ New in 0.9.16:

15 to search.

16* Vect, Fin and So moved out of prelude into base, in modules Data.Vect,

17 Data.Fin and Data.So respectively.

18−

19* Several long-standing issues resolved, particularly with pattern matching

18* Several long-standing issues resolved, particularly with pattern matching

20 and coverage checking.

19 and coverage checking.

20+* Modules can now have API documentation strings.

21

22New in 0.9.15:

23--------------

idris.cabal+7−2

@@ -422,6 +422,11 @@ 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/input

428+ test/idrisdoc009/*.idr

429+

425

430

426 test/interactive001/run

431 test/interactive001/run

427 test/interactive001/input

432 test/interactive001/input

@@ -725,12 +730,12 @@ Library

725 , bytestring < 0.11

730 , bytestring < 0.11

726 , cheapskate < 0.2

731 , cheapskate < 0.2

727 , containers >= 0.5 && < 0.6

732 , containers >= 0.5 && < 0.6

728− , deepseq < 1.4

733+ , deepseq < 1.5

729 , directory >= 1.2 && < 1.3

734 , directory >= 1.2 && < 1.3

730 , filepath < 1.4

735 , filepath < 1.4

731 , fingertree >= 0.1 && < 0.2

736 , fingertree >= 0.1 && < 0.2

732 , haskeline >= 0.7 && < 0.8

737 , haskeline >= 0.7 && < 0.8

733− , lens >= 4.1.1 && < 4.7

738+ , lens >= 4.1.1 && < 4.8

734 , mtl >= 2.2.1 && < 2.3

739 , mtl >= 2.2.1 && < 2.3

735 , network < 2.7

740 , network < 2.7

736 , optparse-applicative >= 0.11 && < 0.12

741 , optparse-applicative >= 0.11 && < 0.12

libs/prelude/Prelude/Uninhabited.idr+3

@@ -1,3 +1,6 @@

1+||| Utilities for working with uninhabited types, to record explicit

2+||| locations for canonical proofs of emptiness. Typically, one should

3+||| use the `absurd` function.

1module Prelude.Uninhabited

4module Prelude.Uninhabited

2

5

3import Builtins

6import Builtins

src/Idris/AbsSyntaxTree.hs+12−1

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

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

166 idris_calledgraph :: Ctxt [Name],

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

168+ idris_moduledocs :: Ctxt (Docstring DocTerm),

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

170+ -- mechanism can be used for disambiguation

168 idris_tyinfodata :: Ctxt TIData,

171 idris_tyinfodata :: Ctxt TIData,

169 idris_fninfo :: Ctxt FnInfo,

172 idris_fninfo :: Ctxt FnInfo,

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

173 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/Core/Unify.hs+4−4

@@ -73,14 +73,14 @@ match_unify ctxt env topx topy inj holes from =

73 let topxn = renameBindersTm env (normalise ctxt env topx)

74 topyn = renameBindersTm env (normalise ctxt env topy) in

75 case runStateT (un [] topxn topyn)

76− (UI 0 []) of

76+ (UI 0 []) of

77 OK (v, UI _ fails) ->

78 do v' <- trimSolutions topx topy from env v

79 return (map (renameBinders env) v')

80 Error e ->

81 -- just normalise the term we're matching against

82 case runStateT (un [] topxn topy)

83− (UI 0 []) of

83+ (UI 0 []) of

84 OK (v, UI _ fails) ->

85 do v' <- trimSolutions topx topy from env v

86 return (map (renameBinders env) v')

@@ -286,12 +286,12 @@ unify ctxt env topx topy inj holes usersupp from =

286 topyn = renameBindersTm env (normalise ctxt env topy) in

287-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

288 case runStateT (un False [] topxn topyn)

289− (UI 0 []) of

289+ (UI 0 []) of

290 OK (v, UI _ fails) ->

291 do v' <- trimSolutions topx topy from env v

292 return (map (renameBinders env) v', reverse fails)

293-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

294− Error e -> tfail e

294+ Error e -> tfail e

295 where

296 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

297 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

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

@@ -225,6 +226,9 @@ ibc i (IBCMetavar n) f =

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

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

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

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

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

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

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

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

231+ _ -> ifail "IBC write failed"

228

232

229process :: Bool -- ^ Reexporting

233process :: Bool -- ^ Reexporting

230 -> IBCFile -> FilePath -> Idris ()

234 -> IBCFile -> FilePath -> Idris ()

@@ -269,6 +273,7 @@ process reexp i fn

269 pTotCheckErr $ force (ibc_totcheckfail i)

273 pTotCheckErr $ force (ibc_totcheckfail i)

270 pCG $ force (ibc_cg i)

274 pCG $ force (ibc_cg i)

271 pDocs $ force (ibc_docstrings i)

275 pDocs $ force (ibc_docstrings i)

276+ pMDocs $ force (ibc_moduledocs i)

272 pCoercions $ force (ibc_coercions i)

277 pCoercions $ force (ibc_coercions i)

273 pTrans $ force (ibc_transforms i)

278 pTrans $ force (ibc_transforms i)

274 pErrRev $ force (ibc_errRev i)

279 pErrRev $ force (ibc_errRev i)

@@ -479,7 +484,12 @@ pDefs reexp syms ds

479 update t = return t

484 update t = return t

480

485

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

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

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

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

488+

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

490+pMDocs ds = mapM_ addMDocStr ds

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

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

483

493

484pAccess :: Bool -- ^ Reexporting?

494pAccess :: Bool -- ^ Reexporting?

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

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

@@ -895,7 +905,7 @@ instance Binary MetaInformation where

895 return (DataMI x1)

905 return (DataMI x1)

896

906

897instance Binary IBCFile where

907instance Binary IBCFile where

898− 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)

908+ 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)

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

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

900 do put x1

910 do put x1

901 put x2

911 put x2

@@ -937,6 +947,7 @@ instance Binary IBCFile where

937 put x38

947 put x38

938 put x39

948 put x39

939 put x40

949 put x40

950+ put x41

940

951

941 get

952 get

942 = do x1 <- get

953 = do x1 <- get

@@ -980,7 +991,8 @@ instance Binary IBCFile where

980 x38 <- get

991 x38 <- get

981 x39 <- get

992 x39 <- get

982 x40 <- get

993 x40 <- get

994+ x41 <- get

983− 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)

995+ 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)

984 else return (initIBC { ver = x1 })

996 else return (initIBC { ver = x1 })

985

997

986instance Binary DataOpt where

998instance Binary DataOpt where

src/Idris/IdeSlave.hs+3−3

@@ -150,9 +150,9 @@ instance SExpable OutputAnnotation where

150 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

151 StringAtom ("Result type is " ++ descr))]

152 where descr = case ordr of

153− EQ -> "isomorphic"

153+ EQ -> "isomorphic"

154− LT -> "more general than searched type"

154+ LT -> "more general than searched type"

155− GT -> "more specific than searched type"

155+ GT -> "more specific than searched type"

156 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]

157

158encodeTerm :: [(Name, Bool)] -> Term -> String

src/Idris/ParseHelpers.hs+8−1

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

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, OverlappingInstances, StandaloneDeriving #-}

1+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, StandaloneDeriving #-}

2+#if !(MIN_VERSION_base(4,8,0))

3+{-# LANGUAGE OverlappingInstances #-}

4+#endif

2module Idris.ParseHelpers where

5module Idris.ParseHelpers where

3

6

4import Prelude hiding (pi)

7import Prelude hiding (pi)

@@ -47,7 +50,11 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

47

50

48deriving instance Parsing IdrisInnerParser

51deriving instance Parsing IdrisInnerParser

49

52

53+#if MIN_VERSION_base(4,8,0)

54+instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

55+#else

50instance TokenParsing IdrisParser where

56instance TokenParsing IdrisParser where

57+#endif

51 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

58 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

52 token p = do s <- get

59 token p = do s <- get

53 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

60 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

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/Primitives.hs+1−1

@@ -20,7 +20,7 @@ data Prim = Prim { p_name :: Name,

20 p_type :: Type,

21 p_arity :: Int,

22 p_def :: [Const] -> Maybe Const,

23− p_lexp :: (Int, PrimFn),

23+ p_lexp :: (Int, PrimFn),

24 p_total :: Totality

25 }

26

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

src/Pkg/PParser.hs+7

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

1+{-# LANGUAGE CPP #-}

2+#if !(MIN_VERSION_base(4,8,0))

1{-# LANGUAGE OverlappingInstances #-}

3{-# LANGUAGE OverlappingInstances #-}

4+#endif

2

5

3module Pkg.PParser where

6module Pkg.PParser where

4

7

@@ -31,7 +34,11 @@ data PkgDesc = PkgDesc { pkgname :: String,

31 }

34 }

32 deriving Show

35 deriving Show

33

36

37+#if MIN_VERSION_base(4,8,0)

38+instance {-# OVERLAPPING #-} TokenParsing PParser where

39+#else

34instance TokenParsing PParser where

40instance TokenParsing PParser where

41+#endif

35 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

42 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

36

43

37

44

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+2

@@ -0,0 +1,2 @@

1+:consolewidth infinite

2+: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