[ fix #2098 ] Allow unclosed comment blocks (#2173)

src/Libraries/Text/Lexer/Core.idr

@@ -15,6 +15,7 @@ export
 data Recognise : (consumes : Bool) -> Type where
      Empty : Recognise False
      Fail : Recognise c
+     EOF : Recognise False
      Lookahead : (positive : Bool) -> Recognise c -> Recognise False
      Pred : (Char -> Bool) -> Recognise True
      SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
@@ -51,6 +52,11 @@ export
 empty : Recognise False
 empty = Empty
 
+||| Recognise end of input
+export
+eof : Recognise False
+eof = EOF
+
 ||| Recognise a character that matches a predicate
 export
 pred : (Char -> Bool) -> Lexer
@@ -99,6 +105,8 @@ export
 scan : Recognise c -> List Char -> List Char -> Maybe (List Char, List Char)
 scan Empty tok str = pure (tok, str)
 scan Fail tok str = Nothing
+scan EOF tok [] = Just (tok,[])
+scan EOF tok (_::_) = Nothing
 scan (Lookahead positive r) tok str
     = if isJust (scan r tok str) == positive
          then pure (tok, str)

src/Parser/Lexer/Source.idr

@@ -126,7 +126,7 @@ mutual
   toEndComment Z = empty
   toEndComment (S k)
                = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
-                        <+> toEndComment (S k)
+                        <+> (eof <|> toEndComment (S k))
              <|> is '{' <+> singleBrace k
              <|> is '-' <+> singleDash k
              <|> stringLit <+> toEndComment (S k)
@@ -136,9 +136,10 @@ mutual
   ||| binder).
   singleBrace : (k : Nat) -> Lexer
   singleBrace k
-     =  is '-' <+> many (is '-')    -- opening delimiter
-               <+> singleDash (S k) -- handles the {----} special case
-    <|> toEndComment (S k)          -- not a valid comment
+     =  is '-' <+> many (is '-')              -- opening delimiter
+               <+> (eof <|> singleDash (S k)) -- `singleDash` handles the {----} special case
+                                              -- `eof` handles the file ending with {---
+    <|> toEndComment (S k)                    -- not a valid comment
 
   ||| After reading a single dash, we may either find another one,
   ||| meaning we may have started reading a line comment, or find
@@ -160,7 +161,7 @@ mutual
         ]
 
 blockComment : Lexer
-blockComment = is '{' <+> is '-' <+> toEndComment 1
+blockComment = is '{' <+> is '-' <+> many (is '-') <+> (eof <|> toEndComment 1)
 
 docComment : Lexer
 docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')

tests/Main.idr

@@ -42,6 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
        "basic061", "basic062", "basic063", "basic064", "basic065",
+       "basic066", "basic067",
        "interpolation001", "interpolation002", "interpolation003",
        "interpolation004"]
 

tests/idris2/basic066/comment.idr

@@ -0,0 +1,12 @@
+{--- -}
+fun : Int -> Bool
+fun x = (x /= 0)
+{-
+-}
+main : IO ()
+main = print (fun 5)
+
+-- EXPLANATION:
+-- this is about parsing the opening `{---`
+-- which used to be parsed as two separate tokens `{-` and `--`
+-- making the above program fail

tests/idris2/basic066/expected

@@ -0,0 +1 @@
+1/1: Building comment (comment.idr)

tests/idris2/basic066/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check comment.idr

tests/idris2/basic067/expected

@@ -0,0 +1,48 @@
+unclosed1.idr
+1/1: Building unclosed1 (unclosed1.idr)
+Main> Main.fun1 : a -> a
+Main> Error: Undefined name fun2. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun2
+        ^^^^
+Did you mean: fun1?
+Main> Error: Undefined name fun3. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun3
+        ^^^^
+Did you mean: fun1?
+Main> Bye for now!
+unclosed2.idr
+1/1: Building unclosed2 (unclosed2.idr)
+Main> Main.fun1 : a -> a
+Main> Error: Undefined name fun2. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun2
+        ^^^^
+Did you mean: fun1?
+Main> Error: Undefined name fun3. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun3
+        ^^^^
+Did you mean: fun1?
+Main> Bye for now!
+unclosed3.idr
+1/1: Building unclosed3 (unclosed3.idr)
+Main> Main.fun1 : a -> a
+Main> Error: Undefined name fun2. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun2
+        ^^^^
+Did you mean: fun1?
+Main> Error: Undefined name fun3. 
+
+(Interactive):1:4--1:8
+ 1 | :t fun3
+        ^^^^
+Did you mean: fun1?
+Main> Bye for now!

tests/idris2/basic067/input

@@ -0,0 +1,4 @@
+:t fun1
+:t fun2
+:t fun3
+:q

tests/idris2/basic067/run

@@ -0,0 +1,8 @@
+rm -rf build
+
+echo "unclosed1.idr"
+$1 --no-color --console-width 0 --no-banner unclosed1.idr < input
+echo "unclosed2.idr"
+$1 --no-color --console-width 0 --no-banner unclosed2.idr < input
+echo "unclosed3.idr"
+$1 --no-color --console-width 0 --no-banner unclosed3.idr < input

tests/idris2/basic067/unclosed1.idr

@@ -0,0 +1,13 @@
+
+fun1 : a -> a
+fun1 x = x
+
+{-
+
+allow unclosed comment block at the end of file
+
+fun2 : a -> a
+fun2 x = x
+
+fun3 : a -> a
+fun3 x = x

tests/idris2/basic067/unclosed2.idr

@@ -0,0 +1,20 @@
+
+fun1 : a -> a
+fun1 x = x
+
+{-
+
+allow unclosed comment block at the end of file
+
+{-
+fun2 : a -> a
+fun2 x = x
+-}
+
+-- Before implemneting #2098, this was somehow parsed as a valid source and `fun3` was in scope
+--
+-- But i don't think that's the supposed behaviour for nested comment blocks?
+-- In any case, after the change, `fun3` now is commented out.
+
+fun3 : a -> a
+fun3 x = x

tests/idris2/basic067/unclosed3.idr

@@ -0,0 +1,15 @@
+
+fun1 : a -> a
+fun1 x = x
+
+{-
+
+allow unclosed comment block at the end of file
+
+{-
+
+fun2 : a -> a
+fun2 x = x
+
+fun3 : a -> a
+fun3 x = x