git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2373 from GuglielmoS/fix/master/doc_should_show_totality_status
df8f605David Christiansen
src/Idris/Docs.hs+25−10
compare with master
unifiedsplit
@@ -53,17 +53,26 @@ showDoc ist d
53 | otherwise = text " -- " <>
53 | otherwise = text " -- " <>
54 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
54 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
55
55
56−pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
56+pprintFD :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
57−pprintFD ist (FD n doc args ty f)
57+pprintFD ist totalityFlag (FD n doc args ty f)
58 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
58 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
59 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
59 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
60 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
60 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
61+ -- show doc
61 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
62 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
63+ -- show fixity
62 maybe empty (\f -> text (show f) <> line) f <>
64 maybe empty (\f -> text (show f) <> line) f <>
65+ -- show arguments doc
63 let argshow = showArgs args [] in
66 let argshow = showArgs args [] in
64− if not (null argshow)
67+ (if not (null argshow)
65 then nest 4 $ text "Arguments:" <$> vsep argshow
68 then nest 4 $ text "Arguments:" <$> vsep argshow
66− else empty)
69+ else empty) <>
70+ -- show totality status
71+ let totality = getTotality in
72+ (if totalityFlag && not (null totality) then
73+ line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
74+ else
75+ empty))
67
76
68 where ppo = ppOptionIst ist
77 where ppo = ppOptionIst ist
69 infixes = idris_infixes ist
78 infixes = idris_infixes ist
@@ -87,15 +96,21 @@ pprintFD ist (FD n doc args ty f)
87 showArgs args ((n, True):bnd)
96 showArgs args ((n, True):bnd)
88 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
97 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
89 showArgs [] _ = []
98 showArgs [] _ = []
99+ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
90
100
101+pprintFDWithTotality :: IState -> FunDoc -> Doc OutputAnnotation
102+pprintFDWithTotality ist = pprintFD ist True
103+
104+pprintFDWithoutTotality :: IState -> FunDoc -> Doc OutputAnnotation
105+pprintFDWithoutTotality ist = pprintFD ist False
91
106
92pprintDocs :: IState -> Docs -> Doc OutputAnnotation
107pprintDocs :: IState -> Docs -> Doc OutputAnnotation
93−pprintDocs ist (FunDoc d) = pprintFD ist d
108+pprintDocs ist (FunDoc d) = pprintFDWithTotality ist d
94pprintDocs ist (DataDoc t args)
109pprintDocs ist (DataDoc t args)
95− = text "Data type" <+> pprintFD ist t <$>
110+ = text "Data type" <+> pprintFDWithoutTotality ist t <$>
96 if null args then text "No constructors."
111 if null args then text "No constructors."
97 else nest 4 (text "Constructors:" <> line <>
112 else nest 4 (text "Constructors:" <> line <>
98− vsep (map (pprintFD ist) args))
113+ vsep (map (pprintFDWithoutTotality ist) args))
99pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)
114pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)
100 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
115 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
101 if nullDocstring doc
116 if nullDocstring doc
@@ -105,12 +120,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct
105 nest 4 (text "Parameters:" <$> prettyParameters)
120 nest 4 (text "Parameters:" <$> prettyParameters)
106 <> line <$>
121 <> line <$>
107 nest 4 (text "Methods:" <$>
122 nest 4 (text "Methods:" <$>
108− vsep (map (pprintFD ist) meths))
123+ vsep (map (pprintFDWithTotality ist) meths))
109 <$>
124 <$>
110 maybe empty
125 maybe empty
111 ((<> line) . nest 4 .
126 ((<> line) . nest 4 .
112 (text "Instance constructor:" <$>) .
127 (text "Instance constructor:" <$>) .
113− pprintFD ist)
128+ pprintFDWithoutTotality ist)
114 ctor
129 ctor
115 <>
130 <>
116 nest 4 (text "Instances:" <$>
131 nest 4 (text "Instances:" <$>
@@ -195,7 +210,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct
195 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
210 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
196
211
197pprintDocs ist (NamedInstanceDoc _cls doc)
212pprintDocs ist (NamedInstanceDoc _cls doc)
198− = nest 4 (text "Named instance:" <$> pprintFD ist doc)
213+ = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist doc)
199
214
200pprintDocs ist (ModDoc mod docs)
215pprintDocs ist (ModDoc mod docs)
201 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
216 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
test/classes001/expected+2
@@ -8,6 +8,7 @@ Methods:
8 myShow : MyShow a => (x : a) -> String
8 myShow : MyShow a => (x : a) -> String
9 The shower
9 The shower
10
10
11+ The function is Total
11Instance constructor:
12Instance constructor:
12 MkMyShow : (myShow : a -> String) -> MyShow a
13 MkMyShow : (myShow : a -> String) -> MyShow a
13 Build a MyShow
14 Build a MyShow
@@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
25
26
26 myShow : a -> String -- The shower
27 myShow : a -> String -- The shower
27
28
29+ The function is Total
test/docs001/expected+1
@@ -8,6 +8,7 @@ Methods:
8 m : C t => t
8 m : C t => t
9 member of class
9 member of class
10
10
11+ The function is Total
11Instances:
12Instances:
12 C A
13 C A
13 instance of class
14 instance of class
test/docs002/expected+3
@@ -1,9 +1,12 @@
1T1 : Type
1T1 : Type
2 Some documentation
2 Some documentation
3
3
4+ The function is Total
4T2 : Type
5T2 : Type
5 Some other documentation
6 Some other documentation
6
7
8+ The function is Total
7T3 : Int
9T3 : Int
8 Some provided postulate
10 Some provided postulate
9
11
12+ The function is not yet checked for totality
test/docs003/expected+1
@@ -8,6 +8,7 @@ Methods:
8 map : Functor f => (m : a -> b) -> f a -> f b
8 map : Functor f => (m : a -> b) -> f a -> f b
9 The action of the functor on morphisms
9 The action of the functor on morphisms
10
10
11+ The function is Total
11Instances:
12Instances:
12 Functor List
13 Functor List
13 Functor Stream
14 Functor Stream
test/docs004/expected+3
@@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
7
7
8 baz : Bool -- A field baz
8 baz : Bool -- A field baz
9
9
10+ The function is Total
10bar : (rec : Foo a) -> Nat
11bar : (rec : Foo a) -> Nat
11 A field bar
12 A field bar
12
13
14+ The function is Total
13baz : (rec : Foo a) -> Bool
15baz : (rec : Foo a) -> Bool
14 A field baz
16 A field baz
15
17
18+ The function is Total
test/interactive005/expected+3
@@ -3,6 +3,7 @@ Hello, World
3main : IO ()
3main : IO ()
4 This is a docstring
4 This is a docstring
5
5
6+ The function is Total
6Main.main is Total
7Main.main is Total
7Hello, World
8Hello, World
8Prelude.Basics.id : a -> a
9Prelude.Basics.id : a -> a
@@ -26,8 +27,10 @@ main : IO ()
26 is a
27 is a
27 docstring
28 docstring
28
29
30+ The function is Total
29main : IO ()
31main : IO ()
30 This is a docstring
32 This is a docstring
31
33
34+ The function is Total
32Nat2 : Type
35Nat2 : Type
33Invalid filename for compiler output "Test.idr"
36Invalid filename for compiler output "Test.idr"