[ fix ] Revert lazy+codata being reserved prims

This reverts part of commit 4febd31c67.

Moved to PR #2992, as this reverted change is separate from adding
`:doc` support for these. There is potentially more discussion to be had
in the new PR.

src/Idris/Parser.idr

@@ -942,16 +942,16 @@ mutual
 
   lazy : OriginDesc -> IndentInfo -> Rule PTerm
   lazy fname indents
-      = do tm <- bounds (decorate fname Typ (lazyPrim "Lazy")
+      = do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
                          *> simpleExpr fname indents)
            pure (PDelayed (boundToFC fname tm) LLazy tm.val)
-    <|> do tm <- bounds (decorate fname Typ (lazyPrim "Inf")
+    <|> do tm <- bounds (decorate fname Typ (exactIdent "Inf")
                          *> simpleExpr fname indents)
            pure (PDelayed (boundToFC fname tm) LInf tm.val)
-    <|> do tm <- bounds (decorate fname Data (lazyPrim "Delay")
+    <|> do tm <- bounds (decorate fname Data (exactIdent "Delay")
                          *> simpleExpr fname indents)
            pure (PDelay (boundToFC fname tm) tm.val)
-    <|> do tm <- bounds (decorate fname Data (lazyPrim "Force")
+    <|> do tm <- bounds (decorate fname Data (exactIdent "Force")
                          *> simpleExpr fname indents)
            pure (PForce (boundToFC fname tm) tm.val)
 
@@ -2322,13 +2322,13 @@ docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
     docLazyPrim =
       let placeholeder : PTerm' Name
           placeholeder = PHole EmptyFC False "lazyDocPlaceholeder"
-      in  do lazyPrim "Lazy"      -- v
+      in  do exactIdent "Lazy"    -- v
              pure (PDelayed EmptyFC LLazy placeholeder)
-      <|> do lazyPrim "Inf"       -- v
+      <|> do exactIdent "Inf"     -- v
              pure (PDelayed EmptyFC LInf placeholeder)
-      <|> do lazyPrim "Delay"
+      <|> do exactIdent "Delay"
              pure (PDelay EmptyFC placeholeder)
-      <|> do lazyPrim "Force"
+      <|> do exactIdent "Force"
              pure (PForce EmptyFC placeholeder)
 
     parse : Rule REPLCmd

src/Parser/Lexer/Source.idr

@@ -65,7 +65,6 @@ data Token
   | CGDirective String
   | EndInput
   | Keyword String
-  | LazyPrim String
   | Pragma String
   | MagicDebugInfo DebugInfo
   | Unrecognised String
@@ -105,7 +104,6 @@ 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
@@ -138,7 +136,6 @@ 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
@@ -249,10 +246,6 @@ 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))
@@ -395,7 +388,6 @@ mutual
     where
       parseIdent : String -> Token
       parseIdent x = if x `elem` keywords then Keyword x
-                     else if x `elem` lazyPrims then LazyPrim x
                      else Ident x
 
       parseNamespace : String -> Token

src/Parser/Rule/Source.idr

@@ -241,14 +241,6 @@ 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
-           lazyPrim "Lazy"
+           exactIdent "Lazy"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelayed (MkFC fname start end) LLazy tm)
     <|> do start <- location
-           lazyPrim "Inf"
+           exactIdent "Inf"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelayed (MkFC fname start end) LInf tm)
     <|> do start <- location
-           lazyPrim "Delay"
+           exactIdent "Delay"
            tm <- simpleExpr fname indents
            end <- location
            pure (IDelay (MkFC fname start end) tm)
     <|> do start <- location
-           lazyPrim "Force"
+           exactIdent "Force"
            tm <- simpleExpr fname indents
            end <- location
            pure (IForce (MkFC fname start end) tm)