[ new ] Implement :doc for laziness primitives

* Restructured the parser to be a bit nicer around these as well
    (subject to approval).

Fixes #2599

CHANGELOG.md

@@ -16,6 +16,8 @@
 ### REPL changes
 
 * Adds documentation for unquotes `~( )`.
+* Adds documentation for laziness and codata primitives: `Lazy`, `Inf`, `Delay`,
+  and `Force`.
 
 ### Backend changes
 

src/Idris/Doc/String.idr

@@ -596,6 +596,56 @@ getDocsForPTerm (PUnquote _ _) = pure $ vcat $
   foo expr = `(either ~(expr) x y)
   ```
   """]
+getDocsForPTerm (PDelayed _ LLazy _) = pure $ vcat $
+  header "Laziness annotation" :: ""
+  :: map (indent 2) [
+  """
+  Indicates that the values of the type should not be computed until absolutely
+  necessary.
+
+  Also causes the compiler to automatically insert Delay/Force calls
+  respectively wherever a computation can be postponed and where a value is
+  necessary. This can be disabled using the `%auto_lazy off` pragma.
+  """
+  ]
+getDocsForPTerm (PDelayed _ LInf  _) = pure $ vcat $
+  header "Codata (infinite data type) annotation" :: ""
+  :: map (indent 2) [
+  """
+  Indicates that the data type may be potentially infinite, e.g. Data.Stream.
+  If the data type IS infinite, it has to be productive, i.e. there has to be at
+  least one non-empty, finite prefix of the type.
+
+  Also causes the compiler to automatically insert Delay/Force calls
+  respectively wherever the next part of a potentially infinite structure
+  occurs, and where we need to look under the next finite prefix of the
+  structure. This can be disabled using the `%auto_lazy off` pragma.
+  """
+  ]
+getDocsForPTerm (PDelay _ _) = pure $ vcat $
+  header "Laziness compiler primitive" :: ""
+  :: map (indent 2) [
+  """
+  For `Lazy` types: postpones the computation until a `Force` requires its
+                    result.
+  For `Inf` types: does not try to deconstruct the next part of the codata
+                   (potentially infinite data structure).
+
+  Automatically inserted by the compiler unless `%auto_lazy off` is set.
+  """
+  ]
+getDocsForPTerm (PForce _ _) = pure $ vcat $
+  header "Laziness compiler primitive" :: ""
+  :: map (indent 2) [
+  """
+  For `Lazy` types: requires the result of a postponed calculation to be
+                    evaluated (see `Delay`).
+  For `Inf` types: deconstructs the next part of the codata (potentially
+                   infinite data structure).
+
+  Automatically inserted by the compiler unless `%auto_lazy off` is set.
+  """
+  ]
 getDocsForPTerm pterm = pure $ "Docs not implemented for" <++> pretty0 (show pterm) <++> "yet"
 
 export

src/Idris/Parser.idr

@@ -942,16 +942,16 @@ mutual
 
   lazy : OriginDesc -> IndentInfo -> Rule PTerm
   lazy fname indents
-      = do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
+      = do tm <- bounds (decorate fname Typ (lazyPrim "Lazy")
                          *> simpleExpr fname indents)
            pure (PDelayed (boundToFC fname tm) LLazy tm.val)
-    <|> do tm <- bounds (decorate fname Typ (exactIdent "Inf")
+    <|> do tm <- bounds (decorate fname Typ (lazyPrim "Inf")
                          *> simpleExpr fname indents)
            pure (PDelayed (boundToFC fname tm) LInf tm.val)
-    <|> do tm <- bounds (decorate fname Data (exactIdent "Delay")
+    <|> do tm <- bounds (decorate fname Data (lazyPrim "Delay")
                          *> simpleExpr fname indents)
            pure (PDelay (boundToFC fname tm) tm.val)
-    <|> do tm <- bounds (decorate fname Data (exactIdent "Force")
+    <|> do tm <- bounds (decorate fname Data (lazyPrim "Force")
                          *> simpleExpr fname indents)
            pure (PForce (boundToFC fname tm) tm.val)
 
@@ -2316,6 +2316,21 @@ docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
     names : List String
     names = extractNames parseCmd
 
+    -- by default, lazy primitives must be followed by a simpleExpr, so we have
+    -- this custom parser for the doc case
+    docLazyPrim : Rule PTerm
+    docLazyPrim =
+      let placeholeder : PTerm' Name
+          placeholeder = PHole EmptyFC False "lazyDocPlaceholeder"
+      in  do lazyPrim "Lazy"      -- v
+             pure (PDelayed EmptyFC LLazy placeholeder)
+      <|> do lazyPrim "Inf"       -- v
+             pure (PDelayed EmptyFC LInf placeholeder)
+      <|> do lazyPrim "Delay"
+             pure (PDelay EmptyFC placeholeder)
+      <|> do lazyPrim "Force"
+             pure (PForce EmptyFC placeholeder)
+
     parse : Rule REPLCmd
     parse = do
       symbol ":"
@@ -2331,7 +2346,10 @@ docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
               <|> TermQuote <$ symbol "`(" <* symbol ")"
               <|> DeclQuote <$ symbol "`[" <* symbol "]"
               )
-        <|> APTerm <$> typeExpr pdef (Virtual Interactive) init
+        <|> APTerm <$> (
+              docLazyPrim
+              <|> typeExpr pdef (Virtual Interactive) init
+              )
       pure (command dir)
 
 declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition

src/Parser/Lexer/Source.idr

@@ -65,6 +65,7 @@ data Token
   | CGDirective String
   | EndInput
   | Keyword String
+  | LazyPrim String
   | Pragma String
   | MagicDebugInfo DebugInfo
   | Unrecognised String
@@ -104,6 +105,7 @@ Show Token where
   show (CGDirective x) = "CGDirective " ++ x
   show EndInput = "end of input"
   show (Keyword x) = x
+  show (LazyPrim x) = x
   show (Pragma x) = "pragma " ++ x
   show (MagicDebugInfo di) = show di
   show (Unrecognised x) = "Unrecognised " ++ x
@@ -136,6 +138,7 @@ Pretty Void Token where
   pretty (CGDirective x) = pretty "CGDirective" <++> pretty x
   pretty EndInput = reflow "end of input"
   pretty (Keyword x) = pretty x
+  pretty (LazyPrim x) = pretty x
   pretty (Pragma x) = pretty "pragma" <++> pretty x
   pretty (MagicDebugInfo di) = pretty (show di)
   pretty (Unrecognised x) = pretty "Unrecognised" <++> pretty x
@@ -246,6 +249,10 @@ keywords = ["data", "module", "where", "let", "in", "do", "record",
             "infixl", "infixr", "infix", "prefix",
             "total", "partial", "covering"]
 
+public export
+lazyPrims : List String
+lazyPrims = ["Lazy", "Inf", "Force", "Delay"]
+
 public export
 debugInfo : List (String, DebugInfo)
 debugInfo = map (\ di => (show di, di))
@@ -388,7 +395,8 @@ mutual
     where
       parseIdent : String -> Token
       parseIdent x = if x `elem` keywords then Keyword x
-                     else Ident x
+                     else if x `elem` lazyPrims then LazyPrim x
+                          else Ident x
 
       parseNamespace : String -> Token
       parseNamespace ns = case mkNamespacedIdent ns of

src/Parser/Rule/Source.idr

@@ -241,6 +241,14 @@ keyword req
                  Keyword s => guard (s == req)
                  _ => Nothing
 
+export
+lazyPrim : String -> Rule ()
+lazyPrim req
+    = terminal ("Unexpected laziness primitive '" ++ req ++ "'") $
+               \case
+                 LazyPrim s => guard (s == req)
+                 _ => Nothing
+
 export
 exactIdent : String -> Rule ()
 exactIdent req

src/TTImp/Parser.idr

@@ -438,22 +438,22 @@ mutual
   lazy : OriginDesc -> IndentInfo -> Rule RawImp
   lazy fname indents
       = do start <- location
-           exactIdent "Lazy"
+           lazyPrim "Lazy"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelayed (MkFC fname start end) LLazy tm)
     <|> do start <- location
-           exactIdent "Inf"
+           lazyPrim "Inf"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelayed (MkFC fname start end) LInf tm)
     <|> do start <- location
-           exactIdent "Delay"
+           lazyPrim "Delay"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelay (MkFC fname start end) tm)
     <|> do start <- location
-           exactIdent "Force"
+           lazyPrim "Force"
            tm <- simpleExpr fname indents
            end <- location
            pure (IForce (MkFC fname start end) tm)