diff --git a/src/Libraries/Text/Lexer/Core.idr b/src/Libraries/Text/Lexer/Core.idr index ec4d321cc..c0f7425b9 100644 --- a/src/Libraries/Text/Lexer/Core.idr +++ b/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) diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 61b5eada5..c5ca20dbb 100644 --- a/src/Parser/Lexer/Source.idr +++ b/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') diff --git a/tests/Main.idr b/tests/Main.idr index 26b1d9dd8..845b5c9f3 100644 --- a/tests/Main.idr +++ b/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"] diff --git a/tests/idris2/basic066/comment.idr b/tests/idris2/basic066/comment.idr new file mode 100644 index 000000000..626af002a --- /dev/null +++ b/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 diff --git a/tests/idris2/basic066/expected b/tests/idris2/basic066/expected new file mode 100644 index 000000000..8da95f265 --- /dev/null +++ b/tests/idris2/basic066/expected @@ -0,0 +1 @@ +1/1: Building comment (comment.idr) diff --git a/tests/idris2/basic066/run b/tests/idris2/basic066/run new file mode 100755 index 000000000..5eb48c2e1 --- /dev/null +++ b/tests/idris2/basic066/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check comment.idr diff --git a/tests/idris2/basic067/expected b/tests/idris2/basic067/expected new file mode 100644 index 000000000..22c7fe6d3 --- /dev/null +++ b/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! diff --git a/tests/idris2/basic067/input b/tests/idris2/basic067/input new file mode 100644 index 000000000..f35ae2699 --- /dev/null +++ b/tests/idris2/basic067/input @@ -0,0 +1,4 @@ +:t fun1 +:t fun2 +:t fun3 +:q diff --git a/tests/idris2/basic067/run b/tests/idris2/basic067/run new file mode 100755 index 000000000..ad57daace --- /dev/null +++ b/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 diff --git a/tests/idris2/basic067/unclosed1.idr b/tests/idris2/basic067/unclosed1.idr new file mode 100644 index 000000000..bcfc56148 --- /dev/null +++ b/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 diff --git a/tests/idris2/basic067/unclosed2.idr b/tests/idris2/basic067/unclosed2.idr new file mode 100644 index 000000000..508df49cf --- /dev/null +++ b/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 diff --git a/tests/idris2/basic067/unclosed3.idr b/tests/idris2/basic067/unclosed3.idr new file mode 100644 index 000000000..0bc17e1f1 --- /dev/null +++ b/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