git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4539 from zgrannan/improve-with-check

Raise an error if too many "with" arguments are provided

commitce61f6073c6df3626a94ed9b18f2ef33929f35e5 authorNiklas Larsson <metaniklas@gmail.com> dateFri 7 Dec 2018, 16:13 (8 years ago) parent011db5f11c1a23
3 files changed+30−3
compare with master
unifiedsplit
src/Idris/Elab/Clause.hs+5−3 test/error006/WithPatsNoWith.idr+11 test/error006/expected+14
src/Idris/Elab/Clause.hs+5−3
@@ -660,11 +660,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
660660 i <- getIState
661661 inf <- isTyInferred fname
662662
663− -- Check if we have "with" patterns outside of "with" block
664− when (isOutsideWith lhs_in && (not $ null withs)) $
663+ -- Check if we have extra "with" patterns
664+ when (not $ null withs) $
665665 ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)
666666 (Elaborating "left hand side of " fname Nothing
667− (Msg "unexpected patterns outside of \"with\" block")))
667+ (Msg $ if isOutsideWith lhs_in
668+ then "unexpected patterns outside of \"with\" block"
669+ else "unexpected extra \"with\" patterns")))
668670
669671 -- get the parameters first, to pass through to any where block
670672 let fn_ty = case lookupTy fname ctxt of
test/error006/WithPatsNoWith.idr+11
@@ -4,3 +4,14 @@ foo : Int -> Bool
44foo 1 | 2 | 3 = True
55foo _ = False
66
7+foo2: Int -> Bool
8+foo2 n with (succ n)
9+ foo2 n | 1 | 2 = True
10+ foo2 _ | _ = False
11+
12+foo3: Int -> Int -> Bool
13+foo3 n m with (succ n)
14+ foo3 _ m | 2 with (succ m)
15+ foo3 _ _ | 2 | 3 | 4 = True
16+ foo3 _ _ | 2 | _ = False
17+ foo3 _ _ | _ = True
test/error006/expected+14
@@ -5,3 +5,17 @@ WithPatsNoWith.idr:4:1-13:
55When checking left hand side of foo:
66unexpected patterns outside of "with" block
77
8+WithPatsNoWith.idr:9:3-16:
9+ |
10+9 | foo2 n | 1 | 2 = True
11+ | ~~~~~~~~~~~~~~
12+When checking left hand side of with block in WithPatsNoWith.foo2:
13+unexpected extra "with" patterns
14+
15+WithPatsNoWith.idr:15:5-24:
16+ |
17+15 | foo3 _ _ | 2 | 3 | 4 = True
18+ | ~~~~~~~~~~~~~~~~~~~~
19+When checking left hand side of with block in with block in WithPatsNoWith.foo3:
20+unexpected extra "with" patterns
21+