918440e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix issue #2666 ("with" patterns accepted outside of "with" block)

Parser parses clauses independently so there is no parsing error in code like this: foo : Int -> Bool foo 1 | 2 | 3 = True foo _ = False Elaborator can check if it sees with patterns but no enclosing with block, so we report error in situations like this.

commit918440e9657158c9a2f1a30fa7adc8ff8a9280a0 authorVitaly Bragilevsky <bravit111@gmail.com> dateThu 29 Oct 2015, 20:47 (11 years ago) parent7b30b6d

4 files changed+22

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+11 test/error006/WithPatsNoWith.idr+6 test/error006/expected+2 test/error006/run+3

src/Idris/Elab/Clause.hs+11

@@ -551,6 +551,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

551551 -- pattern bindings

552552 i <- getIState

553553 inf <- isTyInferred fname

554+

555+ -- Check if we have "with" patterns outside of "with" block

556+ when (isOutsideWith lhs_in && (not $ null withs)) $

557+ ierror $ (At fc (Elaborating "left hand side of " fname Nothing

558+ (Msg "unexpected patterns outside of \"with\" block")))

559+

554560 -- get the parameters first, to pass through to any where block

555561 let fn_ty = case lookupTy fname (tt_ctxt i) of

556562 [t] -> t

@@ -803,6 +809,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

803809 isArg' _ = False

804810 isArg _ _ = False

805811

812+ -- term is not within "with" block

813+ isOutsideWith :: PTerm -> Bool

814+ isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False

815+ isOutsideWith _ = True

816+

806817elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

807818 = do let tcgen = Dictionary `elem` opts

808819 ctxt <- getContext

test/error006/WithPatsNoWith.idrnew file+6

@@ -0,0 +1,6 @@

1+module WithPatsNoWith

3+foo : Int -> Bool

4+foo 1 | 2 | 3 = True

5+foo _ = False

test/error006/expectednew file+2

@@ -0,0 +1,2 @@

1+WithPatsNoWith.idr:4:5:When checking left hand side of foo:

2+unexpected patterns outside of "with" block

test/error006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --consolewidth 80 $@ --check --nocolour WithPatsNoWith.idr

3+rm -f *.ibc