Change :doc to use PTerm instead of Name (#1178)

src/Idris/DocString.idr

@@ -9,6 +9,7 @@ import Idris.Resugar
 import Idris.Syntax
 
 import TTImp.TTImp
+import TTImp.Elab.Prim
 
 import Libraries.Data.ANameMap
 import Data.List
@@ -45,10 +46,19 @@ addDocStringNS ns n_in doc
                            saveDocstrings $= insert n' () } syn)
 
 export
-getDocsFor : {auto c : Ref Ctxt Defs} ->
-             {auto s : Ref Syn SyntaxInfo} ->
-             FC -> Name -> Core (List String)
-getDocsFor fc n
+getDocsForPrimitive : {auto c : Ref Ctxt Defs} ->
+                      {auto s : Ref Syn SyntaxInfo} ->
+                      Constant -> Core (List String)
+getDocsForPrimitive constant = do
+    let (_, type) = checkPrim EmptyFC constant
+    let typeString = show constant ++ " : " ++ show !(resugar [] type)
+    pure [typeString ++ "\n\tPrimitive"]
+
+export
+getDocsForName : {auto c : Ref Ctxt Defs} ->
+                 {auto s : Ref Syn SyntaxInfo} ->
+                 FC -> Name -> Core (List String)
+getDocsForName fc n
     = do syn <- get Syn
          defs <- get Ctxt
          all@(_ :: _) <- lookupCtxtName n (gamma defs)
@@ -149,6 +159,20 @@ getDocsFor fc n
              extra <- getExtra n def
              pure (doc ++ extra)
 
+export
+getDocsForPTerm : {auto c : Ref Ctxt Defs} ->
+                  {auto s : Ref Syn SyntaxInfo} ->
+                  PTerm -> Core (List String)
+getDocsForPTerm (PRef fc name) = getDocsForName fc name
+getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant
+getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
+getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
+getDocsForPTerm (PList _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"]
+getDocsForPTerm (PPair _ _ _) = pure ["Pair Literal\n\tDesugars to MkPair or Pair"]
+getDocsForPTerm (PDPair _ _ _ _) = pure ["Dependant Pair Literal\n\tDesugars to MkDPair or DPair"]
+getDocsForPTerm (PUnit _) = pure ["Unit Literal\n\tDesugars to MkUnit or Unit"]
+getDocsForPTerm pterm = pure ["Docs not implemented for " ++ show pterm ++ " yet"]
+
 summarise : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             Name -> Core String

src/Idris/IDEMode/REPL.idr

@@ -196,7 +196,7 @@ process (MakeCase l n)
 process (MakeWith l n)
     = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n)))
 process (DocsFor n modeOpt)
-    = replWrap $ Idris.REPL.process (Doc (UN n))
+    = replWrap $ Idris.REPL.process (Doc (PRef EmptyFC (UN n)))
 process (Apropos n)
     = do todoCmd "apropros"
          pure $ REPL $ Printed emptyDoc

src/Idris/Parser.idr

@@ -1876,7 +1876,7 @@ parserCommandsForHelp =
   , noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
   , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
   , nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
-  , nameArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name"
+  , exprArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name or primitive"
   , moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) "Browse contents of a namespace"
   , loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
   , autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth "Set the width of the console output (0 for unbounded) (auto by default)"

src/Idris/REPL.idr

@@ -666,7 +666,7 @@ docsOrSignature fc n
          let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
                                      (map fst all)
              | [] => typeSummary defs
-         getDocsFor fc n
+         getDocsForName fc n
   where
     typeSummary : Defs -> Core (List String)
     typeSummary defs = do Just def <- lookupCtxtExact n (gamma defs)
@@ -849,8 +849,8 @@ process (Total n)
                              tot <- getTotality replFC fn >>= toFullNames
                              pure $ (fn, tot))
                                (map fst ts)
-process (Doc n)
-    = do doc <- getDocsFor replFC n
+process (Doc itm)
+    = do doc <- getDocsForPTerm itm
          pure $ Printed $ vsep $ pretty <$> doc
 process (Browse ns)
     = do doc <- getContents ns

src/Idris/Syntax.idr

@@ -449,7 +449,7 @@ data REPLCmd : Type where
      CWD: REPLCmd
      Missing : Name -> REPLCmd
      Total : Name -> REPLCmd
-     Doc : Name -> REPLCmd
+     Doc : PTerm -> REPLCmd
      Browse : Namespace -> REPLCmd
      SetLog : Maybe LogLevel -> REPLCmd
      SetConsoleWidth : Maybe Nat -> REPLCmd

src/Parser/Lexer/Source.idr

@@ -299,7 +299,7 @@ mutual
   rawTokens =
           match comment (const Comment)
       <|> match blockComment (const Comment)
-      <|> match docComment (DocComment . drop 3)
+      <|> match docComment (DocComment . removeOptionalLeadingSpace . drop 3)
       <|> match cgDirective mkDirective
       <|> match holeIdent (\x => HoleIdent (assert_total (strTail x)))
       <|> compose (choice $ exact <$> groupSymbols)
@@ -345,6 +345,11 @@ mutual
       countHashtag : String -> Nat
       countHashtag = count (== '#') . unpack
 
+      removeOptionalLeadingSpace : String -> String
+      removeOptionalLeadingSpace str = case strM str of
+        StrCons ' ' tail => tail
+        _ => str
+
 export
 lexTo : Lexer ->
         String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))

tests/idris2/docs001/expected

@@ -1,45 +1,45 @@
 Main> Prelude.plus : Nat -> Nat -> Nat
-	 Add two natural numbers.
-	 @ x the number to case-split on
-	 @ y the other numberpublic export
+	Add two natural numbers.
+	@ x the number to case-split on
+	@ y the other numberpublic export
 
 Totality: total
 Main> Prelude.Nat : Type
-	 Natural numbers: unbounded, unsigned integers which can be pattern matched.
+	Natural numbers: unbounded, unsigned integers which can be pattern matched.
 
 Constructors:
 Z : Nat
-	 Zero.
+	Zero.
 S : Nat -> Nat
-	 Successor.
+	Successor.
 Main> Prelude.List : Type -> Type
-	 Generic lists.
+	Generic lists.
 
 Constructors:
 Nil : List a
-	 Empty list
+	Empty list
 :: : a -> List a -> List a
 Main> Prelude.Show : Type -> Type
-	 Things that have a canonical `String` representation.
+	Things that have a canonical `String` representation.
 Parameters: ty
 
 Methods:
 show : (x : ty) -> String
-	 Convert a value to its `String` representation.
-	 @ x the value to convert
+	Convert a value to its `String` representation.
+	@ x the value to convert
 showPrec : (d : Prec) -> (x : ty) -> String
-	 Convert a value to its `String` representation in a certain precedence
-	 context.
+	Convert a value to its `String` representation in a certain precedence
+	context.
 	
-	 A value should produce parentheses around itself if and only if the given
-	 precedence context is greater than or equal to the precedence of the
-	 outermost operation represented in the produced `String`.  *This is
-	 different from Haskell*, which requires it to be strictly greater.  `Open`
-	 should thus always produce *no* outermost parens, `App` should always
-	 produce outermost parens except on atomic values and those that provide
-	 their own bracketing, like `Pair` and `List`.
-	 @ d the precedence context.
-	 @ x the value to convert
+	A value should produce parentheses around itself if and only if the given
+	precedence context is greater than or equal to the precedence of the
+	outermost operation represented in the produced `String`.  *This is
+	different from Haskell*, which requires it to be strictly greater.  `Open`
+	should thus always produce *no* outermost parens, `App` should always
+	produce outermost parens except on atomic values and those that provide
+	their own bracketing, like `Pair` and `List`.
+	@ d the precedence context.
+	@ x the value to convert
 
 Implementations:
 	Show Int
@@ -60,8 +60,8 @@ Implementations:
 	Show a => Show (Maybe a)
 	(Show a, Show b) => Show (Either a b)
 Main> Prelude.show : Show ty => ty -> String
-	 Convert a value to its `String` representation.
-	 @ x the value to convert
+	Convert a value to its `String` representation.
+	@ x the value to convert
 
 Totality: total
 Main> Prelude.Monad : (Type -> Type) -> Type
@@ -70,13 +70,15 @@ Constraints: Applicative m
 
 Methods:
 >>= : m a -> (a -> m b) -> m b
-	 Also called `bind`.
+	Also called `bind`.
 join : m (m a) -> m a
-	 Also called `flatten` or mu.
+	Also called `flatten` or mu.
 
 Implementations:
 	Monad IO
 	Monad Maybe
 	Monad (Either e)
 	Monad List
+Main> 1 : Integer
+	Primitive
 Main> Bye for now!

tests/idris2/docs001/input

@@ -4,4 +4,5 @@
 :doc Show
 :doc show
 :doc Monad
+:doc 1
 :q

tests/idris2/docs002/expected

@@ -1,6 +1,6 @@
 1/1: Building Doc (Doc.idr)
 Doc> hello : Int -> Int
-	 Hello!
+	Hello!
 world : Nat -> Nat
-	 World!
+	World!
 Doc> Bye for now!

tests/idris2/interactive019/expected

@@ -11,18 +11,18 @@ Prelude.Show.show : Char -> String
 
 Prelude.Cast.cast : Char -> String
 Main> Prelude.const : a -> b -> a
-	 Constant function.  Ignores its second argument.
+	Constant function.  Ignores its second argument.
 
 Totality: total
 Main> Prelude.toUpper : Char -> Char
-	 Convert a letter to the corresponding upper-case letter, if any.
-	 Non-letters are ignored.
+	Convert a letter to the corresponding upper-case letter, if any.
+	Non-letters are ignored.
 
 Totality: total
 
 Prelude.toLower : Char -> Char
-	 Convert a letter to the corresponding lower-case letter, if any.
-	 Non-letters are ignored.
+	Convert a letter to the corresponding lower-case letter, if any.
+	Non-letters are ignored.
 
 Totality: total
 Main> Bye for now!