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

git.iko.soy/Idris-dev

Elaborate lhs of pattern clause properly in implicit arguments

commit319582e8a9adbb4e85b9c49cde1b631a0e35c20d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Oct 2012, 21:53 (14 years ago) parent4863beb

2 files changed+7−4

unifiedsplit

src/Idris/ElabTerm.hs+5−2

@@ -151,8 +151,11 @@ elab ist info pattern tcgen fn tm

151151 showHd x = show x

152152 elab' ina (PAlternative False as)

153153 = trySeq as

154− where trySeq [] = fail "All alternatives fail to elaborate"

155− trySeq (x : xs) = try (elab' ina x) (trySeq xs)

154+ where -- if none work, take the error from the first

155+ trySeq (x : xs) = let e1 = elab' ina x in

156+ try e1 (trySeq' e1 xs)

157+ trySeq' deferr [] = deferr

158+ trySeq' deferr (x : xs) = try (elab' ina x) (trySeq' deferr xs)

156159 elab' ina (PPatvar fc n) | pattern = patvar n

157160 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

158161 = do ctxt <- get_context

src/Idris/Parser.hs+2−2

@@ -1259,7 +1259,7 @@ pClause syn

12591259 = try (do pushIndent

12601260 n_in <- pfName; let n = expandNS syn n_in

12611261 cargs <- many (pConstraintArg syn)

1262− iargs <- many (pImplicitArg syn)

1262+ iargs <- many (pImplicitArg (syn { inPattern = True } ))

12631263 fc <- pfc

12641264 args <- many (pArgExpr syn)

12651265 wargs <- many (pWExpr syn)

@@ -1297,7 +1297,7 @@ pClause syn

12971297 <|> try (do pushIndent

12981298 n_in <- pfName; let n = expandNS syn n_in

12991299 cargs <- many (pConstraintArg syn)

1300− iargs <- many (pImplicitArg syn)

1300+ iargs <- many (pImplicitArg (syn { inPattern = True } ))

13011301 fc <- pfc

13021302 args <- many (pArgExpr syn)

13031303 wargs <- many (pWExpr syn)