8e1a52c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix error location for lhs for prefix app clauses

8e1a52cJason Felice9 years ago

src/Idris/Elab/Clause.hs+7−4

compare with master

unifiedsplit

@@ -662,8 +662,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

662

663 -- Check if we have "with" patterns outside of "with" block

664 when (isOutsideWith lhs_in && (not $ null withs)) $

665+ ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)

665− ierror (At fc (Elaborating "left hand side of " fname Nothing

666+ (Elaborating "left hand side of " fname Nothing

666− (Msg "unexpected patterns outside of \"with\" block")))

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

667

668

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

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

669 let fn_ty = case lookupTy fname ctxt of

670 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

689 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

690 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

690 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

691 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

691 (do res <- errAt "left hand side of " fname Nothing

692 (do res <- errAt "left hand side of " fname Nothing

693+ (erun (fromMaybe NoFC $ highestFC lhs_in_as)

692− (erun fc (buildTC i info ELHS opts fname

694+ (buildTC i info ELHS opts fname

693 (allNamesIn lhs_in)

695 (allNamesIn lhs_in)

694 (infTerm lhs)))

696 (infTerm lhs)))

695 probs <- get_probs

697 probs <- get_probs

@@ -950,7 +952,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

950 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

952 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

951 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

953 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

952 (errAt "left hand side of with in " fname Nothing

954 (errAt "left hand side of with in " fname Nothing

955+ (erun (fromMaybe NoFC $ highestFC lhs_in)

953− (erun fc (buildTC i info ELHS opts fname

956+ (buildTC i info ELHS opts fname

954 (allNamesIn lhs_in)

957 (allNamesIn lhs_in)

955 (infTerm lhs))) )

958 (infTerm lhs))) )

956 setContext ctxt'

959 setContext ctxt'

src/Idris/Parser.hs+9−9

@@ -1172,18 +1172,19 @@ clause syn

1172 put (ist { lastParse = Just n })

1173 return $ PWith fc n capp wargs wval pn withs)

1174 <|> do pushIndent

1175+ ((n, nfc, args, wargs), lhs_fc) <- withExtent $ do

1175− (n_in, nfc) <- withExtent fnName; let n = expandNS syn n_in

1176+ (n, nfc) <- withExtent (expandNS syn <$> fnName)

1176− args <- many (P.try (implicitArg (syn { inPattern = True } ))

1177+ args <- many (P.try (implicitArg (syn { inPattern = True } ))

1177− <|> P.try (constraintArg (syn { inPattern = True }))

1178+ <|> P.try (constraintArg (syn { inPattern = True }))

1178− <|> (fmap pexp (argExpr syn)))

1179+ <|> (fmap pexp (argExpr syn)))

1179− wargs <- many (wExpr syn)

1180+ wargs <- many (wExpr syn)

1181+ return (n, nfc, args, wargs)

1182+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args

1180 (do (r, fc) <- withExtent (rhs syn n)

1183 (do (r, fc) <- withExtent (rhs syn n)

1181− let capp = PApp fc (PRef nfc [nfc] n) args

1182 let wsyn = syn { syn_namespace = [] }

1184 let wsyn = syn { syn_namespace = [] }

1183 (wheres, nmap) <- whereBlock n wsyn <* popIndent

1185 (wheres, nmap) <- whereBlock n wsyn <* popIndent

1184 <|> ([], []) <$ terminator

1186 <|> ([], []) <$ terminator

1185− ist <- get

1186− put (ist { lastParse = Just n })

1187+ modify $ \ist -> ist { lastParse = Just n }

1187 return $ PClause fc n capp wargs r wheres) <|> (do

1188 return $ PClause fc n capp wargs r wheres) <|> (do

1188 keyword "with"

1189 keyword "with"

1189 ist <- get

1190 ist <- get

@@ -1196,7 +1197,6 @@ clause syn

1196 ds <- some $ fnDecl syn

1197 ds <- some $ fnDecl syn

1197 closeBlock

1198 closeBlock

1198 popIndent

1199 popIndent

1199− let capp = PApp fc (PRef nfc [nfc] n) args

1200 let withs = map (fillLHSD n capp wargs) $ concat ds

1201 return $ PWith fc n capp wargs wval pn withs)

1202 <?> "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:

2unexpected patterns outside of "with" block

test/regression002/expected+10−10

@@ -20,7 +20,7 @@ Specifically:

20 1

21 and

22 0

23−reg010.idr:5:28-31:

23+reg010.idr:5:3-26:

24When checking left hand side of with block in usubst.unsafeSubst:

25Can't match on with block in usubst.unsafeSubst warg a P x x px

26reg018a.idr:16:1-18:

@@ -46,9 +46,9 @@ reg028a.idr:17:14-18:

46This style of tactic proof is deprecated. See %runElab for the replacement.

47reg028a.idr:11:1-14:

48tbad.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:

50Can'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:

52Can't match on foo f x x Refl

53reg035b.idr:8:12-38:No such variable __pi_arg

54reg044.idr:4:6-10:

@@ -84,12 +84,12 @@ No such variable Bogus

84 | ^

85unexpected Operator without known fixity: !!

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:

88When checking an application of constructor Main.MkInfer:

89 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:

91No 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':

93No explicit types on left hand side: Nat

94reg054.idr:40:1-7:When checking left hand side of tctrick:

95When checking an application of Main.tctrick:

@@ -97,14 +97,14 @@ When checking an application of Main.tctrick:

97 Maybe a1 (Type of Just x)

98 and

99 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:

101Can'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:

103Can'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:

105When checking an application of constructor Foo.CAny:

106 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:

108Can't match on apply (\x, y => x) a

109reg056.idr:7:16-25:dodgy n m Refl is a valid case

110reg056.idr:10:11-20:nonk Refl is a valid case