I changed everything but the reflection and builtin stuff. I don't know
enough to mess with that. So there are a bunch of warnings for
Language.Reflection etc.
No need to do this when collecting deferred names, just do it for
display purposes. It's safer anyway, due to potential name clashes in
the normalisation. Fixes#2806
Sometimes elaboration of applications failed unnecessarily because we
assumed they'd have a simple type, and there'd be a strange error
reported if they didn't. Now use proper dependent application, and drop
back to the original simple version if the type of the function can't be
inferred.
Now look at the type of the patterns to infer what the argument type of
the new function should be. This helps if, for example, the scrutinee
function has some type which needs to be resolved to a specific type
class instance, and we can't do this from the scrutinee alone.
At the cost of having to check the result, file IO operations no longer
silently fail, so you won't get a segfault on trying to read a
non-existent file any more.
Pattern matching alternative notation makes this not too painful (see
Prelude.File.readFile for example)
Also, versions which throw exceptions instead could be implemented in
IOExcept, if exceptions are preferred.
Parser parses clauses independently so there is no parsing error
in code like this:
foo : Int -> Bool
foo 1 | 2 | 3 = True
foo _ = False
Elaborator can check if it sees with patterns but no enclosing with block,
so we report error in situations like this.
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
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.
Also improve import chasing, by only following imports in the current
source tree (so not in dependencies we happen to have the source for,
which will be part of other packages)
Names for case block functions (such as "case block in f") now show the
source location from which they originated. This will make it easier to
diagnose problems like totality warnings coming from case blocks,
staging restriction errors from %runElab, and similar.
I'm collecting all the various tactics that I've defined in my various
projects that have proven to be useful and making them into an
includable library, both as an example of Elab reflection and to have a
semi-standard vocabulary.
Any name which would be a valid unbound implicit is now *always* an
unbound implicit. This is much more resilient to changes in inputs, but
does require that function names be explicitly qualified when in
argument position.
Updated libraries/tests accordingly.
WARNING: This is likely to break some code; the fix is, in all cases, to
give explicit namespaces for function names in types in an argument
position (i.e. a valid position for it to be an unbound implicit).
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.
