1c155de · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Print interface constraints as a separate section

commit1c155de55b5259180f07943b88f0ac3653ce2252 authorOskar Wickström <oskar.wickstrom@gmail.com> dateWed 12 Oct 2016, 07:44 (10 years ago) parent9ca1d73

6 files changed+38−9

compare with master

unifiedsplit

src/Idris/Docs.hs+9−8 test/TestData.hs+2−1 test/docs006/docs006.idr+7 test/docs006/expected+16 test/docs006/input+1 test/docs006/run+3

src/Idris/Docs.hs+9−8

@@ -148,6 +148,11 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

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

149149 <> line <$>

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

151+

152+ <> (if null constraints

153+ then empty

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

155+

151156 <> line <$>

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

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

@@ -234,17 +239,13 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

234239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

235240 isSubInterface _ = False

236241

237− prettyConstraints separateLine =

238− let separator = if separateLine then line else empty

239− in case constraints of

240− [] -> empty

241− [pt] -> pprintPTerm ppo params' [] infixes pt <+> text "=>" <> separator

242− _ -> parens (cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))) <+> text "=>" <> separator

242+ prettyConstraints =

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

243244

244245 prettyParameters =

245246 if any (isJust . snd) params

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

247− else prettyConstraints False <+> hsep (punctuate comma (map (prettyName True False params' . fst) params))

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

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

248249

249250pprintDocs ist (RecordDoc n doc ctor projs params)

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

test/TestData.hs+2−1

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

9191 ( 2, ANY ),

9292 ( 3, ANY ),

9393 ( 4, ANY ),

94− ( 5, ANY )]),

94+ ( 5, ANY ),

95+ ( 6, ANY )]),

9596 ("dsl", "DSL",

9697 [ ( 1, ANY ),

9798 ( 2, C_CG ),

test/docs006/docs006.idrnew file+7

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

1+module docs006

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

4+Parameters:

5+ t -- some parameter

7+Constraints:

8+ Eq t

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