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.
These are the features which should not be considered stable:
ElabReflection, DSLNotation, UniquenessTypes and FirstClassReflection,
in addition to the existing TypeProviders and ErrorReflection
* Deprecate "Monad.return" in favor of "pure"
* Update all included libraries to use "pure"
* Update internal code generation to remove "return"
* Remove unused AST constructor PReturn
* Update tests
This adds Quotable implementations for every public datatype in Language.Reflection and Language.Reflection.Elab and for a couple of additional types which are returned by primitive Elab actions (namely Pair and Unit).
Add two new Elab effects:
* declareDatatype, which adds the type constructor declaration to the
context
* defineDatatype, which adds the constructors to the datatype
This makes it possible to write elaborators for term languages that use
Idris's plicity information. As a test of this, the test suite now
includes a mini-implementation of a subset of Agda's reflection using
Elab.
This fixes an obscure issue where certain do-bound names that did not
shadow, but were identical to, other do-bound names in different
subexpressions of one larger expression would fail when referred to in
antiquotations. Example:
(do h <- gensym
claim h a
fill `(C1 ~(Var h)); solve) <|>
(do h <- gensym
claim h b
fill `(C2 ~(Var h)); solve)
The second antiquoted h would throw a "No Such Variable" error, because
the second lambda-bound h was renamed at one point without its use site
being renamed similarly.
Fixes#2217 by demanding that global names in TT terms be
unambiguous. The elaborator will always produce them that way, but user
elab scripts might not, which led to confusion.
Also, disentagle 'apply' and 'fill'.
