ad9ef67 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2775 from bravit/fix/master/withpats

ad9ef67Niklas Larsson11 years ago

src/Idris/Elab/Clause.hs+11

compare with master

unifiedsplit

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

551 -- pattern bindings

552 i <- getIState

553 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+

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

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

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

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

556 [t] -> t

562 [t] -> t

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

803 isArg' _ = False

809 isArg' _ = False

804 isArg _ _ = False

810 isArg _ _ = False

805

811

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

813+ isOutsideWith :: PTerm -> Bool

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

815+ isOutsideWith _ = True

816+

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

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

807 = do let tcgen = Dictionary `elem` opts

818 = do let tcgen = Dictionary `elem` opts

808 ctxt <- getContext

819 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