diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 4a4ce40f9..cb6a2f4ee 100644 --- a/src/Idris/Parser.idr +++ b/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 diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 68fd4d77d..a6d13e6df 100644 --- a/src/Parser/Lexer/Source.idr +++ b/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,8 +388,7 @@ 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 + else Ident x parseNamespace : String -> Token parseNamespace ns = case mkNamespacedIdent ns of diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index ad199d7fb..4b3922b4e 100644 --- a/src/Parser/Rule/Source.idr +++ b/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 diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 0d60c808e..b8a1415fe 100644 --- a/src/TTImp/Parser.idr +++ b/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)