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.
Introduce a new primitive for taking substrings. This can't really be
done efficiently with strTail and strCons, so I think it deserves to
exist as a primitive. Implementations are included for the evaluator as
well as the C and JS backends. Other backends will need to implement it.
Postpone failing searches rather than giving up immediately, since more
information (e.g. type class constraints) may be available when trying
later.
Also improves error reporting of postponed searches by recording what
was being elaborated at the time.
Fixes#2456