Fixes idris-lang#3264 Show auto implicit documentaton in Idris Doc.

cynede · Jul 13, 2016 · 088846b · 088846b
1 parent 96e583c
commit 088846b
Show file tree

Hide file tree

Showing 7 changed files with 123 additions and 43 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -26,6 +26,11 @@
 * The File Effect has been updated to take into account changes in
   `Prelude.File` and to provide a 'better' API.
 
+## Tool updates
+
+* Idris' documentation system now displays the documentation for auto
+  implicits in the output of `:doc`. This is tested for in `docs005`.
+
 # New in 0.12:
 
 ## Language updates

diff --git a/idris.cabal b/idris.cabal
@@ -858,6 +858,15 @@ Extra-source-files:
                        test/docs003/input
                        test/docs003/*.idr
                        test/docs003/expected
+                       test/docs004/run
+                       test/docs004/input
+                       test/docs004/*.idr
+                       test/docs004/expected
+                       test/docs005/run
+                       test/docs005/input
+                       test/docs005/*.idr
+                       test/docs005/expected
+
 
                        benchmarks/ALL
                        benchmarks/*.pl

diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs
@@ -69,49 +69,62 @@ showDoc ist d
                 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
 
 pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
-pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
-    = nest 4 (prettyName True nsFlag [] n <+> colon <+>
-              pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
-                                     , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
-              -- show doc
-              renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
-              -- show fixity
-              maybe empty (\f -> text (show f) <> line) f <>
-              -- show arguments doc
-              let argshow = showArgs args [] in
-              (if not (null argshow)
-                then nest 4 $ text "Arguments:" <$> vsep argshow
-                else empty) <>
-              -- show totality status
-              let totality = getTotality in
-              (if totalityFlag && not (null totality) then
-                line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
-               else
-                empty))
-
-    where ppo = ppOptionIst ist
-          infixes = idris_infixes ist
-          showArgs ((n, ty, Exp {}, Just d):args) bnd
-             = bindingOf n False <+> colon <+>
-               pprintPTerm ppo bnd [] infixes ty <>
-               showDoc ist d <> line
-               :
-               showArgs args ((n, False):bnd)
-          showArgs ((n, ty, Constraint {}, Just d):args) bnd
-             = text "Class constraint" <+>
-               pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
-               :
-               showArgs args ((n, True):bnd)
-          showArgs ((n, ty, Imp {}, Just d):args) bnd
-             = text "(implicit)" <+>
-               bindingOf n True <+> colon <+>
-               pprintPTerm ppo bnd [] infixes ty <>
-               showDoc ist d <> line
-               :
-               showArgs args ((n, True):bnd)
-          showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
-          showArgs []                  _ = []
-          getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
+pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
+          nest 4 (prettyName True nsFlag [] n
+      <+> colon
+      <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
+                             , not (T.isPrefixOf (T.pack "__") n') ] infixes ty
+      -- show doc
+      <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
+      -- show fixity
+      <$> maybe empty (\f -> text (show f) <> line) f
+      -- show arguments doc
+      <> let argshow = showArgs args [] in
+           (if not (null argshow)
+             then nest 4 $ text "Arguments:" <$> vsep argshow
+             else empty)
+      -- show totality status
+      <> let totality = getTotality in
+           (if totalityFlag && not (null totality)
+              then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
+              else empty))
+
+    where
+      ppo = ppOptionIst ist
+
+      infixes = idris_infixes ist
+
+      -- Recurse over and show the Function's Documented arguments
+      showArgs ((n, ty, Exp {}, Just d):args)        bnd = -- Explicitly bound.
+            bindingOf n False
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, False):bnd)
+      showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.
+            text "Class constraint"
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, ty, Imp {}, Just d):args)        bnd = -- Implicit arguments.
+            text "(implicit)"
+        <+> bindingOf n True
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, ty, TacImp{}, Just d):args)      bnd = -- Tacit implicits
+            text "(auto implicit)"
+        <+> bindingOf n True
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, _, _, _):args)                   bnd = -- Anything else
+            showArgs args ((n, True):bnd)
+      showArgs []                                    _   = [] -- end of arguments
+
+      getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
 
 pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
 pprintFDWithTotality ist = pprintFD ist True

diff --git a/test/docs005/docs005.idr b/test/docs005/docs005.idr
@@ -0,0 +1,19 @@
+module docs005
+
+import Data.List
+
+%default total
+
+||| A foobar with an auto implicit
+data Foobar : Type where
+  ||| New Foo
+  |||
+  ||| @xs Some `xs`
+  ||| @ys Some `ys`
+  ||| @prf The prf
+  ||| @prf1 A prf
+  NewFoo : (xs : List String)
+        -> (ys : List Nat)
+        -> {prf1 : NonEmpty xs}
+        -> {auto prf : NonEmpty ys}
+        -> Foobar
diff --git a/test/docs005/expected b/test/docs005/expected
@@ -0,0 +1,29 @@
+Data type docs005.Foobar : Type
+    A foobar with an auto implicit
+
+Constructors:
+    NewFoo : (xs : List String) ->
+        (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
+        New Foo
+        Arguments:
+            xs : List String  -- Some xs
+
+            ys : List Nat  -- Some ys
+
+            (implicit) prf1 : NonEmpty xs  -- A prf
+
+            (auto implicit) prf : NonEmpty ys  -- The prf
+
+docs005.NewFoo : (xs : List String) ->
+    (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
+    New Foo
+    Arguments:
+        xs : List String  -- Some xs
+
+        ys : List Nat  -- Some ys
+
+        (implicit) prf1 : NonEmpty xs  -- A prf
+
+        (auto implicit) prf : NonEmpty ys  -- The prf
+
+    The function is Total
diff --git a/test/docs005/input b/test/docs005/input
@@ -0,0 +1,2 @@
+:doc Foobar
+:doc NewFoo
diff --git a/test/docs005/run b/test/docs005/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} --quiet --nocolor docs005.idr < input
+rm *.ibc