[ re #2038 ] doc for reserved symbols (#2126)

src/Idris/Doc/Keywords.idr

@@ -255,8 +255,8 @@ implicitarg = vcat $
       will return `0` if no argument is passed and its argument otherwise.
     """]
 
-unused : Doc IdrisDocAnn
-unused = "Currently unused keyword"
+unusedKeyword : Doc IdrisDocAnn
+unusedKeyword = "Currently unused keyword"
 
 interfacemechanism : Doc IdrisDocAnn
 interfacemechanism = vcat $
@@ -520,7 +520,7 @@ keywordsDoc =
   :: "record" ::= recordtypes
   :: "auto" ::= implicitarg
   :: "default" ::= implicitarg
-  :: "implicit" ::= unused
+  :: "implicit" ::= unusedKeyword
   :: "mutual" ::= mutualblock
   :: "namespace" ::= namespaceblock
   :: "parameters" ::= parametersblock
@@ -537,7 +537,7 @@ keywordsDoc =
   :: "using" ::= ""
   :: "interface" ::= interfacemechanism
   :: "implementation" ::= interfacemechanism
-  :: "open" ::= unused
+  :: "open" ::= unusedKeyword
   :: "import" ::= importing
   :: "public" ::= visibility
   :: "export" ::= visibility
@@ -556,3 +556,137 @@ getDocsForKeyword : String -> Doc IdrisDocAnn
 getDocsForKeyword k
   = maybe (annotate (Syntax Keyword) $ pretty k) doc
   $ lookup k keywordsDoc
+
+
+unusedSymbol : Doc IdrisDocAnn
+unusedSymbol = "Currently unused symbol"
+
+lambdaAbstraction : Doc IdrisDocAnn
+lambdaAbstraction = """
+  An anonymous function is introduced using a lambda `\\` and binds a
+  comma-separated list of either variable names or irrefutable patterns
+  before returning a right hand side using `=>`.
+
+  For instance we can implement `transport` like so:
+  ```
+  transport : a === b -> a -> b
+  transport = \ Refl, v => v
+  ```
+  """
+
+fatArrow : Doc IdrisDocAnn
+fatArrow = vcat
+  [ """
+    Used for an interface constraint in a type signature or as part of a
+    lambda abstraction or case block.
+
+    1. Interface constraint
+    """
+  , indent 2 """
+    `a => b` corresponds to `{auto _ : a} -> b`
+    """, ""
+  , """
+    2. Lambda abstraction
+    """
+  , indent 2 lambdaAbstraction
+  , "", """
+    3. Case block
+    """
+  ]
+
+bang : Doc IdrisDocAnn
+bang = """
+  Directive to lift the following effectful expression to the nearest enclosing
+  (potentially implicit) `do` block. In the following definition for instance
+
+  ```
+  anyM : Monad m => (a -> m Bool) -> List a -> m (Maybe a)
+  anyM p [] = pure Nothing
+  anyM p (x :: xs) = if !(p x) then pure (Just x) else anyM p xs
+  ```
+
+  the expression `if !(p x) then pure (Just x) else anyM p xs` is equivalent to
+  the following `do` block:
+
+  ```
+  do b <- p x
+     if b then pure (Just x) else anyM p xs
+  ```
+  """
+
+asPattern : Doc IdrisDocAnn
+asPattern = """
+  An as pattern `@` can be used to both pattern match on a variable
+  and retain a name for the compound expression. E.g. instead of writing
+  ```
+  last : List a -> Maybe a
+  last [] = Nothing
+  last [x] = Just x
+  last (x :: y :: ys) = last (y :: ys)
+  ```
+
+  where, in the last clasue, we take `y :: ys` apart on the left hand side
+  before reconstructing it on the right hand side, we can write:
+
+  ```
+  last (x :: xs@(_ :: _)) = last xs
+  ```
+  """
+
+tupleSyntax : Doc IdrisDocAnn
+tupleSyntax = "Used to build dependent pairs together with parentheses"
+
+rangeSyntax : Doc IdrisDocAnn
+rangeSyntax = """
+  The ellipsis `..` can be used to generate lists or streams of values for
+  types that implement the `Range` interface.
+
+  Lists can be generated using an initial value, an (optional) second value
+  and a final one. For instance, we can generate lists of integers like so:
+    1. `[1..5]`   evaluates to `[1,2,3,4,5]`
+    2. `[1,3..5]` evaluates to `[1, 3, 5]`
+
+  Streams can be generated using an initial value and an optional second value.
+  For instance the following streams of integers:
+    1. `[1..]`   for all positive integers
+    2. `[1,3..]` for all positive odds
+  """
+
+symbolsDoc : All DocFor Source.reservedSymbols
+symbolsDoc
+  = "," ::= ""
+  :: ";" ::= ""
+  :: "_" ::= """
+             An implicit value either solved by unification or bound
+             as a pattern or type variable.
+             """
+  :: "`" ::= ""
+  :: tabulate (::= "Grouping symbol (opening token)") ?
+  ++ tabulate (::= "Grouping symbol (closing token)") ?
+  ++ "%" ::= "Start of a pragma"
+  :: "\\" ::= lambdaAbstraction
+  :: ":" ::= """
+             Type declaration, for instance `id : a -> a`
+             declares a new definition `id` of type `a -> a`.
+             """
+  :: "=" ::= "Definition or equality type"
+  :: ":=" ::= "Let binding"
+  :: "|" ::= "Additional patterns showing up in a `with` clause"
+  :: "|||" ::= "Document string attached to the following definition"
+  :: "<-" ::= "Bind in a do block"
+  :: "->" ::= "Function type"
+  :: "=>" ::= fatArrow
+  :: "?" ::= "An implicit value solved by unification."
+  :: "!" ::= bang
+  :: "&" ::= unusedSymbol
+  :: "**" ::= tupleSyntax
+  :: ".." ::= rangeSyntax
+  :: "~" ::= ""
+  :: "@" ::= asPattern
+  :: []
+
+export
+getDocsForSymbol : String -> Doc IdrisDocAnn
+getDocsForSymbol k
+  = maybe (annotate (Syntax Keyword) $ pretty k) doc
+  $ lookup k symbolsDoc

src/Idris/Doc/String.idr

@@ -165,20 +165,20 @@ getDocsForPrimitive constant = do
 
   where
   primDoc : Constant -> Doc IdrisDocAnn
-  primDoc (I i) = "Primitive value"
-  primDoc (I8 i) = "Primitive value"
-  primDoc (I16 i) = "Primitive value"
-  primDoc (I32 i) = "Primitive value"
-  primDoc (I64 i) = "Primitive value"
-  primDoc (BI i) = "Primitive value"
-  primDoc (B8 i) = "Primitive value"
-  primDoc (B16 i) = "Primitive value"
-  primDoc (B32 i) = "Primitive value"
-  primDoc (B64 i) = "Primitive value"
-  primDoc (Str s) = "Primitive value"
-  primDoc (Ch c) = "Primitive value"
-  primDoc (Db d) = "Primitive value"
-  primDoc WorldVal = "Primitive value"
+  primDoc (I i) = "Primitive signed int value (backend-dependent precision)"
+  primDoc (I8 i) = "Primitive signed 8 bits value"
+  primDoc (I16 i) = "Primitive signed 16 bits value"
+  primDoc (I32 i) = "Primitive signed 32 bits value"
+  primDoc (I64 i) = "Primitive signed 64 bits value"
+  primDoc (BI i) = "Primitive unsigned int value (backend-dependent precision)"
+  primDoc (B8 i) = "Primitive unsigned 8 bits value"
+  primDoc (B16 i) = "Primitive unsigned 16 bits value"
+  primDoc (B32 i) = "Primitive unsigned 32 bits value"
+  primDoc (B64 i) = "Primitive unsigned 64 bits value"
+  primDoc (Str s) = "Primitive string value"
+  primDoc (Ch c) = "Primitive character value"
+  primDoc (Db d) = "Primitive double value"
+  primDoc WorldVal = "Primitive token for IO actions"
 
   primDoc IntType = "Primitive type of bounded signed integers (backend dependent size)"
   primDoc Int8Type = "Primitive type of 8 bits signed integers"
@@ -193,7 +193,7 @@ getDocsForPrimitive constant = do
   primDoc StringType = "Primitive type of strings"
   primDoc CharType = "Primitive type of characters"
   primDoc DoubleType = "Primitive type of double-precision floating-points"
-  primDoc WorldType = "Primitive token for IO actions"
+  primDoc WorldType = "Primitive type of tokens for IO actions"
 
 public export
 data Config : Type where
@@ -489,7 +489,7 @@ getDocsForPTerm (PList _ _ _) = pure $ vcat
   ]
 getDocsForPTerm (PSnocList _ _ _) = pure $ vcat
   [ "SnocList Literal"
-  , indent 2 "Desugars to (:<) and Empty"
+  , indent 2 "Desugars to (:<) and Lin"
   ]
 getDocsForPTerm (PPair _ _ _) = pure $ vcat
   [ "Pair Literal"
@@ -512,6 +512,7 @@ getDocs : {auto o : Ref ROpts REPLOpts} ->
           {auto s : Ref Syn SyntaxInfo} ->
           DocDirective -> Core (Doc IdrisDocAnn)
 getDocs (APTerm ptm) = getDocsForPTerm ptm
+getDocs (Symbol k) = pure $ getDocsForSymbol k
 getDocs (Keyword k) = pure $ getDocsForKeyword k
 
 

src/Idris/Parser.idr

@@ -2043,6 +2043,8 @@ docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
       symbol ":"
       runParseCmd parseCmd
       dir <- mustWork $ Keyword <$> anyKeyword
+                    <|> Symbol <$> anyReservedSymbol
+                               <* eoi -- needed so that we don't capture `(<$)`
                     <|> APTerm <$> typeExpr pdef (Virtual Interactive) init
       pure (command dir)
 

src/Idris/Syntax.idr

@@ -584,8 +584,12 @@ data EditCmd : Type where
 
 public export
 data DocDirective : Type where
+  ||| A reserved keyword
   Keyword : String -> DocDirective
-  APTerm : PTerm -> DocDirective
+  ||| A reserved symbol
+  Symbol  : String -> DocDirective
+  ||| An arbitrary PTerm
+  APTerm  : PTerm -> DocDirective
 
 public export
 data REPLCmd : Type where

src/Libraries/Data/List/Quantifiers/Extra.idr

@@ -13,3 +13,13 @@ lookup v (px :: pxs)
   = case decEq (head xs) v of
       No _ => lookup v pxs
       Yes Refl => Just px
+
+export
+(++) : All p xs -> All p ys -> All p (xs ++ ys)
+[] ++ pys = pys
+(px :: pxs) ++ pys = px :: (pxs ++ pys)
+
+export
+tabulate : ((x : a) -> p x) -> (xs : List a) -> All p xs
+tabulate f [] = []
+tabulate f (x :: xs) = f x :: tabulate f xs

src/Parser/Lexer/Source.idr

@@ -224,7 +224,7 @@ keywords = ["data", "module", "where", "let", "in", "do", "record",
 special : List String
 special = ["%lam", "%pi", "%imppi", "%let"]
 
-export
+public export
 symbols : List String
 symbols = [",", ";", "_", "`"]
 
@@ -271,7 +271,7 @@ validSymbol : Lexer
 validSymbol = some (pred isOpChar)
 
 -- Valid symbols which have a special meaning so can't be operators
-export
+public export
 reservedSymbols : List String
 reservedSymbols
     = symbols ++ groupSymbols ++ (groupClose <$> groupSymbols) ++

src/Parser/Rule/Source.idr

@@ -157,7 +157,15 @@ symbol : String -> Rule ()
 symbol req
     = terminal ("Expected '" ++ req ++ "'") $
                \case
-                 Symbol s => if s == req then Just () else Nothing
+                 Symbol s => guard (s == req)
+                 _ => Nothing
+
+export
+anyReservedSymbol : Rule String
+anyReservedSymbol
+  = terminal ("Expected a reserved symbol") $
+               \case
+                 Symbol s => s <$ guard (s `elem` reservedSymbols)
                  _ => Nothing
 
 export
@@ -173,15 +181,15 @@ keyword : String -> Rule ()
 keyword req
     = terminal ("Expected '" ++ req ++ "'") $
                \case
-                 Keyword s => if s == req then Just () else Nothing
+                 Keyword s => guard (s == req)
                  _ => Nothing
 
 export
 exactIdent : String -> Rule ()
 exactIdent req
     = terminal ("Expected " ++ req) $
                \case
-                 Ident s => if s == req then Just () else Nothing
+                 Ident s => guard (s == req)
                  _ => Nothing
 
 export
@@ -278,15 +286,13 @@ reservedNames
 
 isNotReservedName : WithBounds String -> EmptyRule ()
 isNotReservedName x
-    = if x.val `elem` reservedNames
-      then failLoc x.bounds $ "Can't use reserved name \{x.val}"
-      else pure ()
+    = when (x.val `elem` reservedNames) $
+        failLoc x.bounds $ "Can't use reserved name \{x.val}"
 
 isNotReservedSymbol : WithBounds String -> EmptyRule ()
 isNotReservedSymbol x
-    = if x.val `elem` reservedSymbols
-      then failLoc x.bounds $ "Can't use reserved symbol \{x.val}"
-      else pure ()
+    = when (x.val `elem` reservedSymbols) $
+        failLoc x.bounds $ "Can't use reserved symbol \{x.val}"
 
 export
 opNonNS : Rule Name
@@ -300,7 +306,7 @@ opNonNS = do
 
 identWithCapital : (capitalised : Bool) -> WithBounds String ->
                    EmptyRule ()
-identWithCapital b x = if b then isCapitalisedIdent x else pure ()
+identWithCapital b x = when b (isCapitalisedIdent x)
 
 nameWithCapital : (capitalised : Bool) -> Rule Name
 nameWithCapital b = opNonNS <|> do
@@ -395,12 +401,8 @@ Show ValidIndent where
 
 checkValid : ValidIndent -> Int -> EmptyRule ()
 checkValid AnyIndent c = pure ()
-checkValid (AtPos x) c = if c == x
-                            then pure ()
-                            else fail "Invalid indentation"
-checkValid (AfterPos x) c = if c >= x
-                               then pure ()
-                               else fail "Invalid indentation"
+checkValid (AtPos x) c = unless (c == x) $ fail "Invalid indentation"
+checkValid (AfterPos x) c = unless (c >= x) $ fail "Invalid indentation"
 checkValid EndOfBlock c = fail "End of block"
 
 ||| Any token which indicates the end of a statement/block/expression

tests/idris2/docs001/expected

@@ -132,7 +132,7 @@ Main> interface Prelude.Monad : (Type -> Type) -> Type
     Monad (Either e)
     Monad List
 Main> 1 : Integer
-  Primitive value
+  Primitive unsigned int value (backend-dependent precision)
 Main> String : Type
   Primitive type of strings
 Hints: