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

src/Idris/AbsSyntax.hs+3−3

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

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

10831083 pDocs

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

1086− = PInstance doc info f

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

1086+ = PInstance doc argDocs info f

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

10881088 n

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

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

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

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

13021302 where

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+6−5

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

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

603603 -- class name, parameters, method declarations

604604 | PInstance

605− (Docstring (Either Err PTerm))

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

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

606607 SyntaxInfo

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

608609 Name -- class

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

692693declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

696697declared (PDSL n _) = [n]

697698declared (PSyntax _ _) = []

698699declared (PMutual _ ds) = concatMap declared ds

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

711712tldeclared (PMutual _ ds) = concatMap tldeclared ds

712713tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

715716tldeclared _ = []

716717

717718defined :: PDecl -> [Name]

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

727728defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

731732defined (PDSL n _) = [n]

732733defined (PSyntax _ _) = []

733734defined (PMutual _ ds) = concatMap defined ds

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

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

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

17351736 = 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)

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

17381739showDeclImp _ _ = text "..."

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

src/Idris/DeepSeq.hs+4−2

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

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

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

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

159159 rnf x3 `seq`

160160 rnf x4 `seq`

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

161+ rnf x5 `seq`

162+ rnf x6 `seq`

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

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

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

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

3232 | ClassDoc Name d -- class docs

3333 [FunDoc' d] -- method docs

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

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

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

36+ [PTerm] -- subclasses

3637 [PTerm] -- superclasses

3738 | ModDoc [String] -- Module name

3839 d

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

8889 if null args then text "No constructors."

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

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

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

9394 if nullDocstring doc

9495 then empty

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

100101 vsep (map (pprintFD ist) meths))

101102 <$>

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

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

104− else map pprintInstance instances'))

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

105+ else map pprintInstance instances))

105106 <>

106107 (if null subclasses then empty

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

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

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

109110 <>

110111 (if null superclasses then empty

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

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

118119 ppo = ppOptionIst ist

119120 infixes = idris_infixes ist

120121

121− pprintInstance (term, doc) =

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

122123 nest 4 (dumpInstance term <>

123− if nullDocstring doc

124+ (if nullDocstring doc

124125 then empty

125126 else line <>

126127 renderDocstring

127128 (renderDocTerm

128129 (pprintDelab ist)

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

131145

132146 dumpInstance :: PTerm -> Doc OutputAnnotation

133147 dumpInstance = pprintPTerm ppo params' [] infixes

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

151165 isSubclass (PPi _ _ _ pt) = isSubclass pt

152166 isSubclass _ = False

153167

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

155−

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

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

168+ prettyParameters =

169+ if any (isJust . snd) params

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

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

159172

160173pprintDocs ist (ModDoc mod docs)

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

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

197210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

198211 docstr = maybe emptyDocstring fst docStrings

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

200− instanceDocs = map (maybe emptyDocstring fst .

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

201214 listToMaybe .

202215 flip lookupCtxt (idris_docstrings i))

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

205219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

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

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

221+ return $ ClassDoc

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

208224 where

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

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

210226 getDInst _ = Nothing

211227

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+

212235docFun :: Name -> Idris FunDoc

213236docFun n

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

110110

111111 -- TODO: probably should normalise

112112 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

116116 i <- getIState

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

155155

156156 tydecl (PTy _ _ _ _ _ _ _) = True

157157 tydecl _ = False

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

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

159159 instdecl _ = False

160160 clause (PClauses _ _ _ _) = True

161161 clause _ = False

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

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

5252

5353elabInstance :: ElabInfo -> SyntaxInfo ->

5454 Docstring (Either Err PTerm) ->

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

5556 ElabWhat -> -- phase

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

5758 Name -> -- the class

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

5960 PTerm -> -- full instance type

6061 Maybe Name -> -- explicit name

6162 [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

6364 i <- getIState

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

6566 [c] -> return c

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

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

7172 let emptyclass = null (class_methods ci)

7273 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

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

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

7677 case expn of

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

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

149150 Just nm -> nm

150151

151− substInstance ips pnames (PInstance doc 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

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

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

153154

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

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

155156 = case lookupCtxtName n (idris_classes i) of

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

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

233233 | what /= EDefns

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

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

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

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

240240 | what /= ETypes

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

src/Idris/IBC.hs+14−11

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

12481248 put x6

12491249 put x7

12501250 put x8

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

1252− put x1

1253− put x2

1254− put x3

1255− put x4

1256− put x5

1257− put x6

1258− put x7

1259− put x8

1260− put x9

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

1252+ do putWord8 8

1253+ put x1

1254+ put x2

1255+ put x3

1256+ put x4

1257+ put x5

1258+ put x6

1259+ put x7

1260+ put x8

1261+ put x9

1262+ put x10

12611263 PDSL x1 x2 -> do putWord8 9

12621264 put x1

12631265 put x2

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

13521354 x7 <- get

13531355 x8 <- get

13541356 x9 <- get

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

1357+ x10 <- get

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

13561359 9 -> do x1 <- get

13571360 x2 <- get

13581361 return (PDSL x1 x2)

src/Idris/IdrisDoc.hs+5−5

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

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

169169

170170 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

172172 names _ = []

173173

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

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

219219

220220 where getFunDocs (FunDoc f) = [f]

221221 getFunDocs (DataDoc f fs) = f:fs

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

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

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

224224 second (_, x, _, _) = x

225225

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

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

418418 H.h1 $ "Namespaces"

419419 H.ul ! class_ "names" $ do

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

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

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

422422 link = toValue $ path ns

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

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

439439createNsDoc ist ns content out =

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

441441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

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

444444 haveDocs _ = []

445445 -- We cannot do anything without a Doc

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

575575 -> H.Html -- ^ Resulting HTML

576576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577577

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

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

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

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

581581 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

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

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

589589 = 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')

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

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

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

592592collect (d : ds) = d : collect ds

593593collect [] = []

src/Idris/Parser.hs+5−5

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

636636@

637637-}

638638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

639−instance_ syn = do (doc, _)

639+instance_ syn = do (doc, argDocs)

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

641641 fc <- getFC

642642 en <- optional instanceName

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

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

647647 let t = bindList (PPi constraint) cs sc

648648 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]

650650 <?> "instance declaration"

651651 where instanceName :: IdrisParser Name

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

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

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

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

14121412 case x of

1413− PClauses _ _ _ _ -> r

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

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

1413+ PClauses{} -> r

1414+ PClass{} -> r

1415+ PInstance{} -> r

14161416 _ -> x

14171417

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

src/Idris/REPL.hs+2−2

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

811811 fixClauses :: PDecl' t -> PDecl' t

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

813813 PClauses fc opts (getClauseName clause) css

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

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

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

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

816816 fixClauses decl = decl

817817

818818process fn (Undefine names) = undefine names

test/interactive008/expected+3

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

1212Instances:

1313 C A

1414 instance of class

15+ C (D a b)

16+ another instance of class

17+ a -- parameter type

1518*interactive008> Bye bye

test/interactive008/interactive008.idr+8

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

77||| type

88data A = B

99

10+||| type 2

11+data D a b = E

12+

1013||| instance of class

1114instance C A where

1215 m = B

16+

17+||| another instance of class

18+||| @ a parameter type

19+instance C (D a b) where

20+ m = E