284b90b · Idris-dev · git.iko.soy

CHANGELOG.md+2

@@ -57,6 +57,8 @@

57 * New flag `--docdir` provided to show default documentation installation location.

58 * New environment variable `IDRIS_DOC_PATH` to allow specification of an alternative installation path for documentation.

59* Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.

60+* Interface parameter constraints are now printed in the output of `:doc`. This

61+ is tested for in `docs006`.

60

62

61## Miscellaneous updates

63## Miscellaneous updates

62

64

src/Idris/AbsSyntax.hs+3−3

@@ -444,10 +444,10 @@ addImplementation :: Bool -- ^ whether the name is an Integer implementation

444addImplementation int res n i

445 = do ist <- getIState

446 case lookupCtxt n (idris_interfaces ist) of

447− [CI a b c d e f ins fds] ->

447+ [CI a b c d e f g ins fds] ->

448− do let cs = addDef n (CI a b c d e f (addI i ins) fds) (idris_interfaces ist)

448+ do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)

449 putIState $ ist { idris_interfaces = cs }

450− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)

450+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)

451 putIState $ ist { idris_interfaces = cs }

452 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]

453 addI i ins | int = (i, res) : ins

src/Idris/AbsSyntaxTree.hs+1

@@ -1401,6 +1401,7 @@ data InterfaceInfo = CI {

1401 , interface_default_super_interfaces :: [PDecl]

1402 , interface_impparams :: [Name]

1403 , interface_params :: [Name]

1404+ , interface_constraints :: [PTerm]

1404 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

1405 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

1405 , interface_determiners :: [Int]

1406 , interface_determiners :: [Int]

1406 } deriving (Show, Generic)

1407 } deriving (Show, Generic)

src/Idris/Docs.hs+11−2

@@ -49,6 +49,7 @@ data Docs' d = FunDoc (FunDoc' d)

49 | InterfaceDoc Name d -- interface docs

50 [FunDoc' d] -- method docs

51 [(Name, Maybe d)] -- parameters and their docstrings

52+ [PTerm] -- parameter constraints

52 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs

53 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs

53 [PTerm] -- sub interfaces

54 [PTerm] -- sub interfaces

54 [PTerm] -- super interfaces

55 [PTerm] -- super interfaces

@@ -140,13 +141,18 @@ pprintDocs ist (DataDoc t args)

140 if null args then text "No constructors."

141 if null args then text "No constructors."

141 else nest 4 (text "Constructors:" <> line <>

142 else nest 4 (text "Constructors:" <> line <>

142 vsep (map (pprintFDWithoutTotality ist False) args))

143 vsep (map (pprintFDWithoutTotality ist False) args))

143−pprintDocs ist (InterfaceDoc n doc meths params implementations sub_interfaces super_interfaces ctor)

144+pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_interfaces super_interfaces ctor)

144 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>

145 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>

145 if nullDocstring doc

146 if nullDocstring doc

146 then empty

147 then empty

147 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

148 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

148 <> line <$>

149 <> line <$>

149 nest 4 (text "Parameters:" <$> prettyParameters)

150 nest 4 (text "Parameters:" <$> prettyParameters)

151+

152+ <> (if null constraints

153+ then empty

154+ else line <$> nest 4 (text "Constraints:" <$> prettyConstraints))

155+

150 <> line <$>

156 <> line <$>

151 nest 4 (text "Methods:" <$>

157 nest 4 (text "Methods:" <$>

152 vsep (map (pprintFDWithTotality ist False) meths))

158 vsep (map (pprintFDWithTotality ist False) meths))

@@ -233,6 +239,9 @@ pprintDocs ist (InterfaceDoc n doc meths params implementations sub_interfaces s

233 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

234 isSubInterface _ = False

240 isSubInterface _ = False

235

241

242+ prettyConstraints =

243+ cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

244+

236 prettyParameters =

245 prettyParameters =

237 if any (isJust . snd) params

246 if any (isJust . snd) params

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

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

@@ -336,7 +345,7 @@ docInterface n ci

336 SN _ -> return Nothing

345 SN _ -> return Nothing

337 _ -> fmap Just $ docFun ctorN

346 _ -> fmap Just $ docFun ctorN

338 return $ InterfaceDoc

347 return $ InterfaceDoc

339− n docstr mdocs params

348+ n docstr mdocs params (interface_constraints ci)

340 implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

349 implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

341 ctorDocs

350 ctorDocs

342 where

351 where

src/Idris/Elab/Interface.hs+1

@@ -132,6 +132,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

132 addInterface tn (CI cn (map nodoc imethods) defaults idecls

133 (map (\(n, _, _) -> n) impps)

134 (map (\(n, _, _) -> n) ps)

135+ (map snd constraints)

135 [] dets)

136 [] dets)

136

137

137 -- for each constraint, build a top level function to chase it

138 -- for each constraint, build a top level function to chase it

src/Idris/IBC.hs+5−3

@@ -47,7 +47,7 @@ import System.Directory

47import System.FilePath

48

49ibcVersion :: Word16

50−ibcVersion = 150

50+ibcVersion = 151

51

52-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

@@ -2354,7 +2354,7 @@ instance (Binary t) => Binary (PArg' t) where

2354

2355

2356instance Binary InterfaceInfo where

2357− put (CI x1 x2 x3 x4 x5 x6 _ x7)

2357+ put (CI x1 x2 x3 x4 x5 x6 x7 _ x8)

2358 = do put x1

2359 put x2

2360 put x3

@@ -2362,6 +2362,7 @@ instance Binary InterfaceInfo where

2362 put x5

2363 put x6

2364 put x7

2365+ put x8

2365 get

2366 get

2366 = do x1 <- get

2367 = do x1 <- get

2367 x2 <- get

2368 x2 <- get

@@ -2370,7 +2371,8 @@ instance Binary InterfaceInfo where

2370 x5 <- get

2371 x5 <- get

2371 x6 <- get

2372 x6 <- get

2372 x7 <- get

2373 x7 <- get

2374+ x8 <- get

2373− return (CI x1 x2 x3 x4 x5 x6 [] x7)

2375+ return (CI x1 x2 x3 x4 x5 x6 x7 [] x8)

2374

2376

2375instance Binary RecordInfo where

2377instance Binary RecordInfo where

2376 put (RI x1 x2 x3)

2378 put (RI x1 x2 x3)

src/Idris/IdrisDoc.hs+10−10

@@ -167,7 +167,7 @@ removeOrphans list =

167 in filter ((flip S.notMember children) . (\(n, _, _) -> n)) list

168

169 where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

170− names (Just (InterfaceDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

170+ names (Just (InterfaceDoc _ _ fds _ _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

171 names _ = []

172

173-- | Whether a Name names something which should be documented

@@ -215,14 +215,14 @@ referredNss (n, Just d, _) =

215 names = concatMap (extractPTermNames) ts

216 in S.map getNs $ S.fromList names

217

218− where getFunDocs (FunDoc f) = [f]

218+ where getFunDocs (FunDoc f) = [f]

219− getFunDocs (DataDoc f fs) = f:fs

219+ getFunDocs (DataDoc f fs) = f:fs

220− getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs

220+ getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _ _) = fs

221− getFunDocs (RecordDoc _ _ f fs _) = f:fs

221+ getFunDocs (RecordDoc _ _ f fs _) = f:fs

222− getFunDocs (NamedImplementationDoc _ fd) = [fd]

222+ getFunDocs (NamedImplementationDoc _ fd) = [fd]

223− getFunDocs (ModDoc _ _) = []

223+ getFunDocs (ModDoc _ _) = []

224− types (FD _ _ args t _) = t:(map second args)

224+ types (FD _ _ args t _) = t:(map second args)

225− second (_, x, _, _) = x

225+ second (_, x, _, _) = x

226

227

228-- | Returns an NsDict of containing all known namespaces and their contents

@@ -576,7 +576,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

576 -> H.Html -- ^ Resulting HTML

577createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

578

579−createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ c) = do

579+createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ _ c) = do

580 H.dt ! (A.id $ toValue $ show n) $ do

581 H.span ! class_ "word" $ do "interface"; nbsp

582 H.span ! class_ "name type"

test/TestData.hs+2−1

@@ -91,7 +91,8 @@ testFamiliesData = [

91 ( 2, ANY ),

92 ( 3, ANY ),

93 ( 4, ANY ),

94− ( 5, ANY )]),

94+ ( 5, ANY ),

95+ ( 6, ANY )]),

95 ("dsl", "DSL",

96 ("dsl", "DSL",

96 [ ( 1, ANY ),

97 [ ( 1, ANY ),

97 ( 2, C_CG ),

98 ( 2, C_CG ),

test/docs006/docs006.idrnew file+7

@@ -0,0 +1,7 @@

1+module docs006

2+

3+||| interface

4+||| @ t some parameter

5+interface Eq t => Foo t where

6+ ||| member of interface

7+ m : t

test/docs006/expectednew file+16

@@ -0,0 +1,16 @@

1+Interface Foo

2+ interface

3+

4+Parameters:

5+ t -- some parameter

6+

7+Constraints:

8+ Eq t

9+

10+Methods:

11+ m : Foo t => t

12+ member of interface

13+

14+ The function is Total

15+Implementations:

16+ <no implementations>

test/docs006/inputnew file+1

@@ -0,0 +1 @@

1+:doc Foo

test/docs006/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

3+rm *.ibc