Fixes#116. This is the solution Idris 1 took, and while it is a special
case, the syntax does make it explicit (in a way) that the result of the
case is unused - if you mean something other than (), you must now say
so!
Another one from the "stop trying to be clever" files :). Instead of a
continuation for fallthrough in the evaluator, be explicit about whether
there's a result, no match, or evaluation is stuck.
Fixes#70
This is quite fiddly as it the blocks might be in different contexts so
we need to keep track of which variables correspond in the scrutinees of
the blocks. Once that's done, check the terms at the leaves convert,
then check the corresponding variables convert.
This may not be perfect yet, because we only look at case scrutinees to
find correspondence. It might also be a bit slower than it could be, but
at least these checks are quite rare.
Fixes#208 and maybe some others?
Allows quoting a term back to a TTImp. Test reflection007 shows one
possible use for this, building a reflected, type safe, representation
of an expression.
On the LHS, we want to match against the reflected thing, so FC and
implicits need to turn into match anything patterns, or we won't match
anything at all. This means we can put quoted terms on the LHS, with
pattern variables under ~().
This invokes a script of type Elab (). %runElan in a term invokes a
script of type Elab TT. The elaborator now pushes in that type, so that
it'll report an appropriate error if you give it a script of the wrong
type.
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
Add %runElab and start on scripts, although all they can do so far is
check a term. This does gives us, sort of, "template Idris" (as
demonstrated in test reflection002)
Don't get too excited yet - I want this in so that it doesn't get too
out of sync, but I still have to think about exactly how it's going to
work in practice.
This is mostly to make it easier to write linear function types without
having to invent names for everything, which might be noisy. Also it
improves the display of linear function types when the name isn't used
in the scope.
I don't know how complete this is, but it certainly detects some of the
most obvious cases which are most likely to be bugs.
While I'm at it, this is as good a time as any to add a general way of
reporting warnings, similar to the way of reporting errors.
Still a couple of things to resolve in coverage and totality checking
before we can switch on %default, so don't expect quite the right
behaviour just yet. More progress though!
Also working on this has caught a few totality errors in the Idris 2
code base that Idris 1 missed... so these are fixed on the way.
The hack (optimisation?) to normalise integer literals when below some
threshold is fine on the RHS, but on the LHS causes problems since we
need them in normal form for pattern matching. Fixes#112
This improves coverage checking, because it can now see that things like
(Z = S x) and (x = S x) are empty. Previously, it only checked that all
possible constructors had a disjoint index. Now, it looks for matches
and checks for disjointness in the matches, which catches a lot more
things especially with equality.
As in Idris 1 - if an interface declares a method as total or covering,
then all implementations have to satisfy that.
Temporarily turn off %default directive again, at least until totality
checking works as it should (this is probably better than removing it
from various places because I'll forget to put them back)
This means temporarily removing some '%default total' from the libraries
and tests, since the input for codata checking isn't right yet (it needs
appropriate use of inlining)
Should have done this ages ago, it was much easier than I expected...
this adds an explicit error clause before running the pattern match
compiler for runtime case trees, but only if the coverage checker finds
there are missing cases.
