7ba4da0 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -1082,8 +1082,8 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

1082 (map (mapsnd (expandParams dec ps ns [])) params)

1083 pDocs

1084 (map (expandParamsD rhs ist dec ps ns) decls)

1085−expandParamsD rhs ist dec ps ns (PInstance doc info f cs n params ty cn decls)

1085+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1086− = PInstance doc info f

1086+ = PInstance doc argDocs info f

1087 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1088 n

1089 (map (expandParams dec ps ns []) params)

@@ -1300,7 +1300,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1300 getImps (Bind n (Pi _ t _) sc) imps

1301 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1302 where

1303− argInfo n (Imp opt _ _ _) Placeholder

1303+ argInfo n (Imp opt _ _ _) Placeholder

1304 = (True, PImp 0 True opt n Placeholder)

1305 argInfo n (Imp opt _ _ _) t'

1306 = (False, PImp (getPriority i t') True opt n t')

src/Idris/AbsSyntaxTree.hs+6−5

@@ -602,7 +602,8 @@ data PDecl' t

602 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

603 -- class name, parameters, method declarations

604 | PInstance

605− (Docstring (Either Err PTerm))

605+ (Docstring (Either Err PTerm)) -- Instance docs

606+ [(Name, Docstring (Either Err PTerm))] -- Parameter docs

606 SyntaxInfo

607 SyntaxInfo

607 FC [(Name, t)] -- constraints

608 FC [(Name, t)] -- constraints

608 Name -- class

609 Name -- class

@@ -692,7 +693,7 @@ declared (PParams _ _ ds) = concatMap declared ds

692declared (PNamespace _ ds) = concatMap declared ds

693declared (PNamespace _ ds) = concatMap declared ds

693declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

694declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

694declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

695declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

695−declared (PInstance _ _ _ _ _ _ _ _ _) = []

696+declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

696declared (PDSL n _) = [n]

697declared (PDSL n _) = [n]

697declared (PSyntax _ _) = []

698declared (PSyntax _ _) = []

698declared (PMutual _ ds) = concatMap declared ds

699declared (PMutual _ ds) = concatMap declared ds

@@ -711,7 +712,7 @@ tldeclared (PParams _ _ ds) = []

711tldeclared (PMutual _ ds) = concatMap tldeclared ds

712tldeclared (PMutual _ ds) = concatMap tldeclared ds

712tldeclared (PNamespace _ ds) = concatMap tldeclared ds

713tldeclared (PNamespace _ ds) = concatMap tldeclared ds

713tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

714tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

714−tldeclared (PInstance _ _ _ _ _ _ _ _ _) = []

715+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

715tldeclared _ = []

716tldeclared _ = []

716

717

717defined :: PDecl -> [Name]

718defined :: PDecl -> [Name]

@@ -727,7 +728,7 @@ defined (PParams _ _ ds) = concatMap defined ds

727defined (PNamespace _ ds) = concatMap defined ds

728defined (PNamespace _ ds) = concatMap defined ds

728defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

729defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

729defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

730defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

730−defined (PInstance _ _ _ _ _ _ _ _ _) = []

731+defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

731defined (PDSL n _) = [n]

732defined (PDSL n _) = [n]

732defined (PSyntax _ _) = []

733defined (PSyntax _ _) = []

733defined (PMutual _ ds) = concatMap defined ds

734defined (PMutual _ ds) = concatMap defined ds

@@ -1733,7 +1734,7 @@ showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <>

1733showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1734showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1734showDeclImp o (PClass _ _ _ cs n ps _ ds)

1735showDeclImp o (PClass _ _ _ cs n ps _ ds)

1735 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1736 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1736−showDeclImp o (PInstance _ _ _ cs n _ t _ ds)

1737+showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1737 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1738 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1738showDeclImp _ _ = text "..."

1739showDeclImp _ _ = text "..."

1739-- showDeclImp (PImport o) = "import " ++ o

1740-- showDeclImp (PImport o) = "import " ++ o

src/Idris/DeepSeq.hs+4−2

@@ -153,12 +153,14 @@ instance (NFData t) => NFData (PDecl' t) where

153 = rnf x1 `seq`

154 rnf x2 `seq`

155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

156− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9)

156+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157 = rnf x1 `seq`

158 rnf x2 `seq`

159 rnf x3 `seq`

160 rnf x4 `seq`

161+ rnf x5 `seq`

162+ rnf x6 `seq`

161− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

163+ rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

162 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+40−17

@@ -32,7 +32,8 @@ data Docs' d = FunDoc (FunDoc' d)

32 | ClassDoc Name d -- class docs

33 [FunDoc' d] -- method docs

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

35− [(PTerm, Docstring DocTerm)] -- instances and docs

35+ [(PTerm, (d, [(Name, d)]))] -- instances

36+ [PTerm] -- subclasses

36 [PTerm] -- superclasses

37 [PTerm] -- superclasses

37 | ModDoc [String] -- Module name

38 | ModDoc [String] -- Module name

38 d

39 d

@@ -88,7 +89,7 @@ pprintDocs ist (DataDoc t args)

88 if null args then text "No constructors."

89 if null args then text "No constructors."

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

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

90 vsep (map (pprintFD ist) args))

91 vsep (map (pprintFD ist) args))

91−pprintDocs ist (ClassDoc n doc meths params instances superclasses)

92+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

92 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

93 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

93 if nullDocstring doc

94 if nullDocstring doc

94 then empty

95 then empty

@@ -100,12 +101,12 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

100 vsep (map (pprintFD ist) meths))

101 vsep (map (pprintFD ist) meths))

101 <$>

102 <$>

102 nest 4 (text "Instances:" <$>

103 nest 4 (text "Instances:" <$>

103− vsep (if null instances' then [text "<no instances>"]

104+ vsep (if null instances then [text "<no instances>"]

104− else map pprintInstance instances'))

105+ else map pprintInstance instances))

105 <>

106 <>

106 (if null subclasses then empty

107 (if null subclasses then empty

107 else line <$> nest 4 (text "Subclasses:" <$>

108 else line <$> nest 4 (text "Subclasses:" <$>

108− vsep (map (dumpInstance . prettifySubclasses . fst) subclasses)))

109+ vsep (map (dumpInstance . prettifySubclasses) subclasses)))

109 <>

110 <>

110 (if null superclasses then empty

111 (if null superclasses then empty

111 else line <$> nest 4 (text "Default superclass instances:" <$>

112 else line <$> nest 4 (text "Default superclass instances:" <$>

@@ -118,16 +119,29 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

118 ppo = ppOptionIst ist

119 ppo = ppOptionIst ist

119 infixes = idris_infixes ist

120 infixes = idris_infixes ist

120

121

121− pprintInstance (term, doc) =

122+ pprintInstance (term, (doc, argDocs)) =

122 nest 4 (dumpInstance term <>

123 nest 4 (dumpInstance term <>

123− if nullDocstring doc

124+ (if nullDocstring doc

124 then empty

125 then empty

125 else line <>

126 else line <>

126 renderDocstring

127 renderDocstring

127 (renderDocTerm

128 (renderDocTerm

128 (pprintDelab ist)

129 (pprintDelab ist)

129 (normaliseAll (tt_ctxt ist) []))

130 (normaliseAll (tt_ctxt ist) []))

130− doc)

131+ doc) <>

132+ if null argDocs

133+ then empty

134+ else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

135+

136+ prettyInstanceParam params (name, doc) =

137+ if nullDocstring doc

138+ then empty

139+ else prettyName True False (zip params (repeat False)) name <+>

140+ showDoc ist doc

141+

142+-- if any (isJust . snd) params

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

144+-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))

131

145

132 dumpInstance :: PTerm -> Doc OutputAnnotation

146 dumpInstance :: PTerm -> Doc OutputAnnotation

133 dumpInstance = pprintPTerm ppo params' [] infixes

147 dumpInstance = pprintPTerm ppo params' [] infixes

@@ -151,11 +165,10 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

151 isSubclass (PPi _ _ _ pt) = isSubclass pt

165 isSubclass (PPi _ _ _ pt) = isSubclass pt

152 isSubclass _ = False

166 isSubclass _ = False

153

167

154− (subclasses, instances') = partition (isSubclass . fst) instances

168+ prettyParameters =

155−

156− prettyParameters = if any (isJust . snd) params

169+ if any (isJust . snd) params

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

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

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

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

159

172

160pprintDocs ist (ModDoc mod docs)

173pprintDocs ist (ModDoc mod docs)

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

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

@@ -197,18 +210,28 @@ docClass n ci

197 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

198 docstr = maybe emptyDocstring fst docStrings

211 docstr = maybe emptyDocstring fst docStrings

199 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

212 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

200− instanceDocs = map (maybe emptyDocstring fst .

213+ instanceDocs = map (fromMaybe (emptyDocstring, []) .

201 listToMaybe .

214 listToMaybe .

202 flip lookupCtxt (idris_docstrings i))

215 flip lookupCtxt (idris_docstrings i))

203 (class_instances ci)

216 (class_instances ci)

204− instances = map (delabTy i) (class_instances ci)

217+ instances = zip (map (delabTy i) (class_instances ci)) instanceDocs

218+ (subclasses, instances') = partition (isSubclass . fst) instances

205 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

206 mdocs <- mapM (docFun . fst) (class_methods ci)

220 mdocs <- mapM (docFun . fst) (class_methods ci)

221+ return $ ClassDoc

207− return $ ClassDoc n docstr mdocs params (zip instances instanceDocs) superclasses

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

208 where

224 where

209− getDInst (PInstance _ _ _ _ _ _ t _ _) = Just t

225+ getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

210 getDInst _ = Nothing

226 getDInst _ = Nothing

211

227

228+ isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

229+ = nm == n && map getTm args == map getTm args'

230+ isSubclass (PPi _ _ _ pt)

231+ = isSubclass pt

232+ isSubclass _

233+ = False

234+

212docFun :: Name -> Idris FunDoc

235docFun :: Name -> Idris FunDoc

213docFun n

236docFun n

214 = do i <- getIState

237 = do i <- getIState

src/Idris/Elab/Class.hs+2−2

@@ -110,7 +110,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

110

111 -- TODO: probably should normalise

112 checkDefaultSuperclassInstance :: PDecl -> Idris ()

113− checkDefaultSuperclassInstance (PInstance _ _ fc cs n ps _ _ _)

113+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n ps _ _ _)

114 = do when (not $ null cs) . tclift

115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116 i <- getIState

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155

156 tydecl (PTy _ _ _ _ _ _ _) = True

157 tydecl _ = False

158− instdecl (PInstance _ _ _ _ _ _ _ _ _) = True

158+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

159 instdecl _ = False

160 clause (PClauses _ _ _ _) = True

161 clause _ = False

src/Idris/Elab/Instance.hs+6−5

@@ -52,6 +52,7 @@ import Util.Pretty(pretty, text)

52

53elabInstance :: ElabInfo -> SyntaxInfo ->

54 Docstring (Either Err PTerm) ->

55+ [(Name, Docstring (Either Err PTerm))] ->

55 ElabWhat -> -- phase

56 ElabWhat -> -- phase

56 FC -> [(Name, PTerm)] -> -- constraints

57 FC -> [(Name, PTerm)] -> -- constraints

57 Name -> -- the class

58 Name -> -- the class

@@ -59,7 +60,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

59 PTerm -> -- full instance type

60 PTerm -> -- full instance type

60 Maybe Name -> -- explicit name

61 Maybe Name -> -- explicit name

61 [PDecl] -> Idris ()

62 [PDecl] -> Idris ()

62−elabInstance info syn doc what fc cs n ps t expn ds = do

63+elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

63 i <- getIState

64 i <- getIState

64 (n, ci) <- case lookupCtxtName n (idris_classes i) of

65 (n, ci) <- case lookupCtxtName n (idris_classes i) of

65 [c] -> return c

66 [c] -> return c

@@ -70,7 +71,7 @@ elabInstance info syn doc what fc cs n ps t expn ds = do

70 let iname = mkiname n (namespace info) ps expn

71 let iname = mkiname n (namespace info) ps expn

71 let emptyclass = null (class_methods ci)

72 let emptyclass = null (class_methods ci)

72 when (what /= EDefns || (null ds && not emptyclass)) $ do

73 when (what /= EDefns || (null ds && not emptyclass)) $ do

73− nty <- elabType' True info syn doc [] fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname t

74 -- if the instance type matches any of the instances we have already,

75 -- if the instance type matches any of the instances we have already,

75 -- and it's not a named instance, then it's overlapping, so report an error

76 -- and it's not a named instance, then it's overlapping, so report an error

76 case expn of

77 case expn of

@@ -148,10 +149,10 @@ elabInstance info syn doc what fc cs n ps t expn ds = do

148 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

149 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

149 Just nm -> nm

150 Just nm -> nm

150

151

151− substInstance ips pnames (PInstance doc syn _ cs n ps t expn ds)

152+ substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)

152− = PInstance doc syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

153+ = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

153

154

154− isOverlapping i (PInstance doc syn _ _ n ps t expn _)

155+ isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)

155 = case lookupCtxtName n (idris_classes i) of

156 = case lookupCtxtName n (idris_classes i) of

156 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

157 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

157 case lookupTy iname (tt_ctxt i) of

158 case lookupTy iname (tt_ctxt i) of

src/Idris/ElabDecls.hs+2−2

@@ -233,9 +233,9 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

233 | what /= EDefns

234 = do iLOG $ "Elaborating class " ++ show n

235 elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

236−elabDecl' what info (PInstance doc s f cs n ps t expn ds)

236+elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238− elabInstance info s doc what f cs n ps t expn ds

238+ elabInstance info s doc argDocs what f cs n ps t expn ds

239elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

240 | what /= ETypes

241 = do iLOG $ "Elaborating record " ++ show tyn

src/Idris/IBC.hs+14−11

@@ -1248,16 +1248,18 @@ instance (Binary t) => Binary (PDecl' t) where

1248 put x6

1249 put x7

1250 put x8

1251− PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 -> do putWord8 8

1251+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252+ do putWord8 8

1252− put x1

1253+ put x1

1253− put x2

1254+ put x2

1254− put x3

1255+ put x3

1255− put x4

1256+ put x4

1256− put x5

1257+ put x5

1257− put x6

1258+ put x6

1258− put x7

1259+ put x7

1259− put x8

1260+ put x8

1260− put x9

1261+ put x9

1262+ put x10

1261 PDSL x1 x2 -> do putWord8 9

1263 PDSL x1 x2 -> do putWord8 9

1262 put x1

1264 put x1

1263 put x2

1265 put x2

@@ -1352,7 +1354,8 @@ instance (Binary t) => Binary (PDecl' t) where

1352 x7 <- get

1354 x7 <- get

1353 x8 <- get

1355 x8 <- get

1354 x9 <- get

1356 x9 <- get

1357+ x10 <- get

1355− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9)

1358+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

1356 9 -> do x1 <- get

1359 9 -> do x1 <- get

1357 x2 <- get

1360 x2 <- get

1358 return (PDSL x1 x2)

1361 return (PDSL x1 x2)

src/Idris/IdrisDoc.hs+5−5

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

168 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169

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

171− names (Just (ClassDoc _ _ fds _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

171+ names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

172 names _ = []

173

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

@@ -219,7 +219,7 @@ referredNss (n, Just d, _) =

219

220 where getFunDocs (FunDoc f) = [f]

221 getFunDocs (DataDoc f fs) = f:fs

222− getFunDocs (ClassDoc _ _ fs _ _ _) = fs

222+ getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223 types (FD _ _ args t _) = t:(map second args)

224 second (_, x, _, _) = x

225

@@ -417,7 +417,7 @@ createIndex nss out =

417 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

418 H.h1 $ "Namespaces"

419 H.ul ! class_ "names" $ do

420− let path ns = "docs" </> genRelNsPath ns "html"

420+ let path ns = "docs" </> genRelNsPath ns "html"

421 item ns = do let n = toHtml $ nsName2Str ns

422 link = toValue $ path ns

423 H.li $ H.a ! href link ! class_ "code" $ n

@@ -439,7 +439,7 @@ createNsDoc :: IState -- ^ Needed to determine the types of names

439createNsDoc ist ns content out =

440 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

443 haveDocs (_, Just d, _) = [d]

444 haveDocs _ = []

445 -- We cannot do anything without a Doc

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

575 -> H.Html -- ^ Resulting HTML

576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577

578−createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

578+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

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

580 H.span ! class_ "word" $ do "class"; nbsp

581 H.span ! class_ "name type"

src/Idris/ParseHelpers.hs+2−2

@@ -587,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588collect (PClass doc f s cs n ps pdocs ds : ds')

589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

590−collect (PInstance doc f s cs n ps t en ds : ds')

590+collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591− = PInstance doc f s cs n ps t en (collect ds) : collect ds'

591+ = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592collect (d : ds) = d : collect ds

593collect [] = []

src/Idris/Parser.hs+5−5

@@ -636,7 +636,7 @@ InstanceName ::= '[' Name ']';

636@

637-}

638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

639−instance_ syn = do (doc, _)

639+instance_ syn = do (doc, argDocs)

640 <- try (docstring syn <* reserved "instance")

641 fc <- getFC

642 en <- optional instanceName

@@ -646,7 +646,7 @@ instance_ syn = do (doc, _)

646 let sc = PApp fc (PRef fc cn) (map pexp args)

647 let t = bindList (PPi constraint) cs sc

648 ds <- option [] (instanceBlock syn)

649− return [PInstance doc syn fc cs cn args t en ds]

649+ return [PInstance doc argDocs syn fc cs cn args t en ds]

650 <?> "instance declaration"

651 where instanceName :: IdrisParser Name

652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -1410,9 +1410,9 @@ loadSource lidr f toline

1410 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1411 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1412 case x of

1413− PClauses _ _ _ _ -> r

1413+ PClauses{} -> r

1414− PClass _ _ _ _ _ _ _ _ -> r

1414+ PClass{} -> r

1415− PInstance _ _ _ _ _ _ _ _ _ -> r

1415+ PInstance{} -> r

1416 _ -> x

1417

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

src/Idris/REPL.hs+2−2

@@ -811,8 +811,8 @@ process fn (NewDefn decls) = do

811 fixClauses :: PDecl' t -> PDecl' t

812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

813 PClauses fc opts (getClauseName clause) css

814− fixClauses (PInstance doc syn fc constraints cls parms ty instName decls) =

814+ fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

815− PInstance doc syn fc constraints cls parms ty instName (map fixClauses decls)

815+ PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

816 fixClauses decl = decl

817

818process fn (Undefine names) = undefine names

test/interactive008/expected+3

@@ -12,4 +12,7 @@ Methods:

12Instances:

13 C A

14 instance of class

15+ C (D a b)

16+ another instance of class

17+ a -- parameter type

15*interactive008> Bye bye

18*interactive008> Bye bye

test/interactive008/interactive008.idr+8

@@ -7,6 +7,14 @@ class C (t : Type) where

7||| type

8data A = B

9

10+||| type 2

11+data D a b = E

12+

10||| instance of class

13||| instance of class

11instance C A where

14instance C A where

12 m = B

15 m = B

16+

17+||| another instance of class

18+||| @ a parameter type

19+instance C (D a b) where

20+ m = E