From 00067e81510cd38354ec5b6333d5bafcb2d21e6e Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Mon, 22 Feb 2021 18:46:35 +0000 Subject: [PATCH] [ fix #637 ] force indentation after a `with` --- libs/base/Data/Nat/Order.idr | 4 ++-- libs/base/Decidable/Equality.idr | 4 ++-- libs/contrib/Data/List/Views/Extra.idr | 16 ++++++++-------- src/Idris/Parser.idr | 2 +- src/Parser/Rule/Source.idr | 26 +++++++++++++++++++++++++- tests/Main.idr | 2 +- tests/idris2/with004/Issue637-2.idr | 8 ++++++++ tests/idris2/with004/Issue637-3.idr | 6 ++++++ tests/idris2/with004/Issue637.idr | 6 ++++++ tests/idris2/with004/expected | 24 ++++++++++++++++++++++++ tests/idris2/with004/input | 2 ++ tests/idris2/with004/run | 5 +++++ 12 files changed, 90 insertions(+), 15 deletions(-) create mode 100644 tests/idris2/with004/Issue637-2.idr create mode 100644 tests/idris2/with004/Issue637-3.idr create mode 100644 tests/idris2/with004/Issue637.idr create mode 100644 tests/idris2/with004/expected create mode 100644 tests/idris2/with004/input create mode 100755 tests/idris2/with004/run diff --git a/libs/base/Data/Nat/Order.idr b/libs/base/Data/Nat/Order.idr index 5a945c05e..55d98a1ba 100644 --- a/libs/base/Data/Nat/Order.idr +++ b/libs/base/Data/Nat/Order.idr @@ -58,8 +58,8 @@ decideLTE (S x) Z = No zeroNeverGreater decideLTE (S x) (S y) with (decEq (S x) (S y)) decideLTE (S x) (S y) | Yes eq = rewrite eq in Yes (reflexive (S y)) decideLTE (S x) (S y) | No _ with (decideLTE x y) - decideLTE (S x) (S y) | No _ | Yes nLTEm = Yes (LTESucc nLTEm) - decideLTE (S x) (S y) | No _ | No nGTm = No (ltesuccinjective nGTm) + decideLTE (S x) (S y) | No _ | Yes nLTEm = Yes (LTESucc nLTEm) + decideLTE (S x) (S y) | No _ | No nGTm = No (ltesuccinjective nGTm) public export implementation Decidable 2 [Nat,Nat] LTE where diff --git a/libs/base/Decidable/Equality.idr b/libs/base/Decidable/Equality.idr index 034c32d4a..02ab0b433 100644 --- a/libs/base/Decidable/Equality.idr +++ b/libs/base/Decidable/Equality.idr @@ -116,8 +116,8 @@ DecEq a => DecEq (List1 a) where decEq (x ::: xs) (y ::: ys) with (decEq x y) decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective) decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys) - decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective) - decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys) + decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective) + decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys) -- TODO: Other prelude data types diff --git a/libs/contrib/Data/List/Views/Extra.idr b/libs/contrib/Data/List/Views/Extra.idr index 128335f30..48a421950 100644 --- a/libs/contrib/Data/List/Views/Extra.idr +++ b/libs/contrib/Data/List/Views/Extra.idr @@ -161,12 +161,12 @@ lazyFilterRec pred (x :: xs) with (pred x) -> {auto prf2 : NonEmpty rest} -> LazyFilterRec (reverse reverseOfSkipped ++ rest) filterHelper revSkipped (y :: xs) with (pred y) - filterHelper revSkipped (y :: xs) | True = - Found (reverse revSkipped) y (lazyFilterRec pred xs) - filterHelper revSkipped (y :: []) | False = - rewrite sym (reverseOntoSpec [y] revSkipped) in - Exhausted $ reverse (y :: revSkipped) - filterHelper revSkipped (y :: (z :: zs)) | False = - rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in + filterHelper revSkipped (y :: xs) | True = + Found (reverse revSkipped) y (lazyFilterRec pred xs) + filterHelper revSkipped (y :: []) | False = rewrite sym (reverseOntoSpec [y] revSkipped) in - filterHelper (y :: revSkipped) (z :: zs) + Exhausted $ reverse (y :: revSkipped) + filterHelper revSkipped (y :: (z :: zs)) | False = + rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in + rewrite sym (reverseOntoSpec [y] revSkipped) in + filterHelper (y :: revSkipped) (z :: zs) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 8d7a1404e..e6abe6267 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -841,7 +841,7 @@ mutual flags <- bounds (withFlags) symbol "(" wval <- bracketedExpr fname flags indents - ws <- nonEmptyBlock (clause (S withArgs) fname) + ws <- mustWork $ nonEmptyBlockAfter col (clause (S withArgs) fname) pure (flags, wval, forget ws)) (flags, wval, ws) <- pure b.val let fc = boundToFC fname (mergeBounds start b) diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 0cd906590..14ba13521 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -438,7 +438,11 @@ blockAfter mincol item else blockEntries (AtPos col) item export -blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> SourceEmptyRule (Maybe hd, List ty) +blockWithOptHeaderAfter : + (column : Int) -> + (header : IndentInfo -> Rule hd) -> + (item : IndentInfo -> Rule ty) -> + SourceEmptyRule (Maybe hd, List ty) blockWithOptHeaderAfter {ty} mincol header item = do symbol "{" commit @@ -472,3 +476,23 @@ nonEmptyBlock item res <- blockEntry (AtPos col) item ps <- blockEntries (snd res) item pure (fst res ::: ps) + +||| `nonEmptyBlockAfter col rule` parses a non-empty `rule`-block indented +||| by at least `col` spaces (unless the block is explicitly delimited +||| by curly braces). `rule` is a function of the actual indentation +||| level. +export +nonEmptyBlockAfter : Int -> (IndentInfo -> Rule ty) -> Rule (List1 ty) +nonEmptyBlockAfter mincol item + = do symbol "{" + commit + res <- blockEntry AnyIndent item + ps <- blockEntries (snd res) item + symbol "}" + pure (fst res ::: ps) + <|> do col <- column + let False = col <= mincol + | True => fail "Expected an indented non-empty block" + res <- blockEntry (AtPos col) item + ps <- blockEntries (snd res) item + pure (fst res ::: ps) diff --git a/tests/Main.idr b/tests/Main.idr index 39438dd2f..9f58740f9 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -153,7 +153,7 @@ idrisTests = MkTestPool [] "total001", "total002", "total003", "total004", "total005", "total006", "total007", "total008", "total009", "total010", -- The 'with' rule - "with001", "with002", + "with001", "with002", "with004", -- with-disambiguation "with003"] diff --git a/tests/idris2/with004/Issue637-2.idr b/tests/idris2/with004/Issue637-2.idr new file mode 100644 index 000000000..e54188916 --- /dev/null +++ b/tests/idris2/with004/Issue637-2.idr @@ -0,0 +1,8 @@ +namespace A + export + foo3 : Int -> Int + foo3 x with (x + 1) + foo3 x | y = y + x + +foo4 : Int +foo4 = A.foo3 5 diff --git a/tests/idris2/with004/Issue637-3.idr b/tests/idris2/with004/Issue637-3.idr new file mode 100644 index 000000000..5225c9271 --- /dev/null +++ b/tests/idris2/with004/Issue637-3.idr @@ -0,0 +1,6 @@ +foo5 : Int -> Int +foo5 x with (x + 1) +foo5 x | y = y + x + +foo6 : Int +foo6 = 52 diff --git a/tests/idris2/with004/Issue637.idr b/tests/idris2/with004/Issue637.idr new file mode 100644 index 000000000..326210a6e --- /dev/null +++ b/tests/idris2/with004/Issue637.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo x with (x + 1) + foo x | y = y + x + +foo2 : Int +foo2 = foo 5 diff --git a/tests/idris2/with004/expected b/tests/idris2/with004/expected new file mode 100644 index 000000000..d9c6fcad2 --- /dev/null +++ b/tests/idris2/with004/expected @@ -0,0 +1,24 @@ +1/1: Building Issue637 (Issue637.idr) +Main> 11 +Main> +Bye for now! +1/1: Building Issue637-2 (Issue637-2.idr) +Error: Expected an indented non-empty block. + +Issue637-2.idr:5:3--5:4 + 1 | namespace A + 2 | export + 3 | foo3 : Int -> Int + 4 | foo3 x with (x + 1) + 5 | foo3 x | y = y + x + ^ + +1/1: Building Issue637-3 (Issue637-3.idr) +Error: Expected an indented non-empty block. + +Issue637-3.idr:3:1--3:2 + 1 | foo5 : Int -> Int + 2 | foo5 x with (x + 1) + 3 | foo5 x | y = y + x + ^ + diff --git a/tests/idris2/with004/input b/tests/idris2/with004/input new file mode 100644 index 000000000..25f21400d --- /dev/null +++ b/tests/idris2/with004/input @@ -0,0 +1,2 @@ +foo2 +:q \ No newline at end of file diff --git a/tests/idris2/with004/run b/tests/idris2/with004/run new file mode 100755 index 000000000..033e0f613 --- /dev/null +++ b/tests/idris2/with004/run @@ -0,0 +1,5 @@ +$1 --no-color --console-width 0 --no-banner Issue637.idr < input +$1 --no-color --console-width 0 --no-banner --check Issue637-2.idr +$1 --no-color --console-width 0 --no-banner --check Issue637-3.idr + +rm -rf build