git.iko.soy/Idris-dev
on master help sign in
Fix error location for lhs for prefix app clauses
commit8e1a52cd3e638b701295625368400381d08ddb40 authorJason Felice <jason.m.felice@gmail.com> dateSun 3 Dec 2017, 10:34 (9 years ago) parentef47811
4 files changed+27−24
compare with master
unifiedsplit
src/Idris/Elab/Clause.hs+7−4 src/Idris/Parser.hs+9−9 test/error006/expected+1−1 test/regression002/expected+10−10
src/Idris/Elab/Clause.hs+7−4
@@ -662,8 +662,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
662662
663663 -- Check if we have "with" patterns outside of "with" block
664664 when (isOutsideWith lhs_in && (not $ null withs)) $
665− ierror (At fc (Elaborating "left hand side of " fname Nothing
666− (Msg "unexpected patterns outside of \"with\" block")))
665+ ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)
666+ (Elaborating "left hand side of " fname Nothing
667+ (Msg "unexpected patterns outside of \"with\" block")))
667668
668669 -- get the parameters first, to pass through to any where block
669670 let fn_ty = case lookupTy fname ctxt of
@@ -689,7 +690,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
689690 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-
690691 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
691692 (do res <- errAt "left hand side of " fname Nothing
692− (erun fc (buildTC i info ELHS opts fname
693+ (erun (fromMaybe NoFC $ highestFC lhs_in_as)
694+ (buildTC i info ELHS opts fname
693695 (allNamesIn lhs_in)
694696 (infTerm lhs)))
695697 probs <- get_probs
@@ -950,7 +952,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
950952 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
951953 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
952954 (errAt "left hand side of with in " fname Nothing
953− (erun fc (buildTC i info ELHS opts fname
955+ (erun (fromMaybe NoFC $ highestFC lhs_in)
956+ (buildTC i info ELHS opts fname
954957 (allNamesIn lhs_in)
955958 (infTerm lhs))) )
956959 setContext ctxt'
src/Idris/Parser.hs+9−9
@@ -1172,18 +1172,19 @@ clause syn
11721172 put (ist { lastParse = Just n })
11731173 return $ PWith fc n capp wargs wval pn withs)
11741174 <|> do pushIndent
1175− (n_in, nfc) <- withExtent fnName; let n = expandNS syn n_in
1176− args <- many (P.try (implicitArg (syn { inPattern = True } ))
1177− <|> P.try (constraintArg (syn { inPattern = True }))
1178− <|> (fmap pexp (argExpr syn)))
1179− wargs <- many (wExpr syn)
1175+ ((n, nfc, args, wargs), lhs_fc) <- withExtent $ do
1176+ (n, nfc) <- withExtent (expandNS syn <$> fnName)
1177+ args <- many (P.try (implicitArg (syn { inPattern = True } ))
1178+ <|> P.try (constraintArg (syn { inPattern = True }))
1179+ <|> (fmap pexp (argExpr syn)))
1180+ wargs <- many (wExpr syn)
1181+ return (n, nfc, args, wargs)
1182+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args
11801183 (do (r, fc) <- withExtent (rhs syn n)
1181− let capp = PApp fc (PRef nfc [nfc] n) args
11821184 let wsyn = syn { syn_namespace = [] }
11831185 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11841186 <|> ([], []) <$ terminator
1185− ist <- get
1186− put (ist { lastParse = Just n })
1187+ modify $ \ist -> ist { lastParse = Just n }
11871188 return $ PClause fc n capp wargs r wheres) <|> (do
11881189 keyword "with"
11891190 ist <- get
@@ -1196,7 +1197,6 @@ clause syn
11961197 ds <- some $ fnDecl syn
11971198 closeBlock
11981199 popIndent
1199− let capp = PApp fc (PRef nfc [nfc] n) args
12001200 let withs = map (fillLHSD n capp wargs) $ concat ds
12011201 return $ PWith fc n capp wargs wval pn withs)
12021202 <?> "function clause"
test/error006/expected+1−1
@@ -1,2 +1,2 @@
1−WithPatsNoWith.idr:4:15-20:When checking left hand side of foo:
1+WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:
22unexpected patterns outside of "with" block
test/regression002/expected+10−10
@@ -20,7 +20,7 @@ Specifically:
2020 1
2121 and
2222 0
23−reg010.idr:5:28-31:
23+reg010.idr:5:3-26:
2424When checking left hand side of with block in usubst.unsafeSubst:
2525Can't match on with block in usubst.unsafeSubst warg a P x x px
2626reg018a.idr:16:1-18:
@@ -46,9 +46,9 @@ reg028a.idr:17:14-18:
4646This style of tactic proof is deprecated. See %runElab for the replacement.
4747reg028a.idr:11:1-14:
4848tbad.qsort' is possibly not total due to: with block in tbad.qsort'
49−reg034.idr:6:16-21:When checking left hand side of bar:
49+reg034.idr:6:1-14:When checking left hand side of bar:
5050Can't match on bar xs xs Refl
51−reg034.idr:9:16-21:When checking left hand side of foo:
51+reg034.idr:9:1-14:When checking left hand side of foo:
5252Can't match on foo f x x Refl
5353reg035b.idr:8:12-38:No such variable __pi_arg
5454reg044.idr:4:6-10:
@@ -84,12 +84,12 @@ No such variable Bogus
8484 | ^
8585unexpected Operator without known fixity: !!
8686
87−reg054.idr:18:19-24:When checking left hand side of inf:
87+reg054.idr:18:1-17:When checking left hand side of inf:
8888When checking an application of constructor Main.MkInfer:
8989 Attempting concrete match on polymorphic argument: 0
90−reg054.idr:34:20-24:When checking left hand side of weird:
90+reg054.idr:34:1-18:When checking left hand side of weird:
9191No explicit types on left hand side: Char
92−reg054.idr:37:32-34:When checking left hand side of weird':
92+reg054.idr:37:1-30:When checking left hand side of weird':
9393No explicit types on left hand side: Nat
9494reg054.idr:40:1-7:When checking left hand side of tctrick:
9595When checking an application of Main.tctrick:
@@ -97,14 +97,14 @@ When checking an application of Main.tctrick:
9797 Maybe a1 (Type of Just x)
9898 and
9999 a (Expected type)
100−reg055.idr:5:9-11:When checking left hand side of g:
100+reg055.idr:5:1-7:When checking left hand side of g:
101101Can't match on g (f 0)
102−reg055.idr:8:7-9:When checking left hand side of h:
102+reg055.idr:8:1-5:When checking left hand side of h:
103103Can't match on h x x
104−reg055a.idr:8:20-23:When checking left hand side of foo:
104+reg055a.idr:8:1-18:When checking left hand side of foo:
105105When checking an application of constructor Foo.CAny:
106106 Attempting concrete match on polymorphic argument: Nothing
107−reg055a.idr:13:25-27:When checking left hand side of Foo.apply:
107+reg055a.idr:13:1-23:When checking left hand side of Foo.apply:
108108Can't match on apply (\x, y => x) a
109109reg056.idr:7:16-25:dodgy n m Refl is a valid case
110110reg056.idr:10:11-20:nonk Refl is a valid case