Commit Graph

12 Commits

Author SHA1 Message Date
Niklas Larsson
b5a6637da8 Rename expected, input and run
Because cabal's wildcards are broken and doesn't allow
files without file endings.
2020-01-25 01:44:54 +01:00
Jason Felice
79351ee7ae Add blank line after "large" messages 2017-12-07 10:18:07 -05:00
Jason Felice
7d0c06b108 Put source code before error (like parse errors) 2017-12-07 10:18:05 -05:00
Jason Felice
f967817d5b Make warnings, non-parse errors pretty 2017-12-07 10:18:02 -05:00
Jason Felice
b1a4264f7c Improve error message locations (#4210)
This contribution uses the strict WriterT transformer over our parser stack with a
monoid over FC and what used to be spanFC to compute the span of
non-terminal parsers from the spans of trackExtent-wrapped parsers.

The net result is that the locations reported for errors and warnings is
much improved. Most errors now report the extent of the error, rather than a
point roughly preceeding it (or after it, sometimes). There are still cases
where FCs are recomputed as a point after parsing--I didn't fix these, to cut
the scope of this PR--though all file locations produced during parsing use
the new, spanning parsing combinators.

I would start reading at Idris.Parser.Stack, then Idris.Parser.Helpers.

Overview:    
- *FC and non-*FC parsers (e.g. tokenFC and token, charLiteralFC and
    charLiteral, etc.) have been elided and the FC suffix removed. Any
    parser can be asked to report it's FC using the extent or withExtent
    combinators.
    
- Extents reported for errors end at the last character of the token, rather
    than on the following character.
 
- Now that all parsers can be queried for their spans, highlighting is
    done with the highlight parser combinator, e.g.
    highlight AnnQuasiquote (symbol "`{{" ...). These can be nested.
   
- Totality checking, in its current design, reports the extent of the first
    equation. This is a bit more misleading now that the span is computed
    correctly, since it could look like it's trying to indicate which clause is
    non-total. We should fix this (hopefully as a separate PR.)
   
- The span of clauses is actually the span of the right-hand side, and so this
    is reported when there is an error on the right-hand side or the left-hand
    side. We should also fix this (hopefully as a separate PR.)
    
- There's probably cases where, owning to the improved granularity, we will now
    notice errors were reported with FCs from the wrong object.
    I haven't tested an IDE-mode client yet. They may need to be patched if they
    are manually excluding the last character of tokens. Highlighting appears to
    work fine without changes, though.
2017-11-30 12:18:36 +01:00
Echo Nolan
4ab3eefdda Remove redundant --consolewidth settings in tests 2016-02-15 17:03:34 -08:00
Niklas Larsson
b0e8b1258b make the tests respect the IDRIS env variable
Simplify the sandbox lookup and only run it once.

Only run the test script once for 'make test' instead of using the
makefile to iterate.
2016-01-22 06:57:04 +01:00
Edwin Brady
4d0a065f86 Change "class/instance" keywords
To "interface/implementation". Old syntax is still valid but gives a
deprecation warning.
2016-01-13 11:18:33 +00:00
Edwin Brady
da914af83e Consistency of implicit/pattern name binding rules
We've always said that the rules for binding names in patterns are the
same as the rules for binding names in implicits, i.e. a name beginning
with a lower case letter, not applied to anything, will be bound
implicitly, or treated as a pattern variable. This hasn't actually
always been quite true, even though it was supposed to be...

Correspondingly, added a warning for constructor names which may be
unexpectedly bound implicitly.

This patch changes the pattern binding rules so that it is the case.
Fixes #2653
2015-10-17 18:44:00 +01:00
David Raymond Christiansen
752a2fcc77 Update tests for proof deprecation 2015-09-10 12:01:39 +02:00
Jan de Muijnck-Hughes
5ea6aa0520 Address semantic differences in putting things to STDOUT.
The changes are as follows:

+ `print` is for putting showable things to STDOUT.
+ `printLn` is for putting showable things to STDOUT with a new line
+ `putCharLn` for putting a single character to STDOUT, with a new line.

Effects has been updated accordingly.
2015-03-06 17:26:33 +00:00
Edwin Brady
7cea995306 Add tests for tutorial examples 2014-03-23 15:21:28 +00:00