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.
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
Get the names of local variables. and add the ability to look up their
types.
When we get a reflected TTImp, either checking the Goal or looking up a
type, it's not impossible that there'll be some repeated binder names,
so also make sure binders are unique relative to the current context.
Ideally we'd also rename things in the environment to guarantee that all
names are unique, but we don't yet.
(This would be much easier if reflected terms were typed such that they
were well scoped, but that would also make reflection harder to use.)
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'.
If available (sometimes, say a top level expression, it might need
inferring so there'll be no goal available). Also add the ability to log
the current goal, or indeed any term.
Still all they can do is check and log. Now scripts must return
something of type TT, which is in practice a TTImp that goes to the
elaborator for final checking
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)
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
Now all common console IO functions available from the
prelude are available through the `Control.App.Console`
interface.
Added:
- putChar
- getChar
- getCharLn
- print
- printLn
Renamed:
- getStr to getLine
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 means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.
There are more flags we want on with (well, at least one: "proof")
The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.
Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.
If we're going to use assert_total. we might as well not have the
distinction between empty and non empty results, which only makes the
code harder to follow.
Also there's some kind of issue which seems to mean the token list can't
be erased if we do that. I will investigate if I can make a smaller
example.
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)
This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
things were being imported that shouldn't have been. The new way is
correct!
An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
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.
For the same behaviour as Idris 1, the primitive cast should return 0 if
the integer is out of bounds. (We should probably drop the Cast
implementation though, since ideally they won't be lossy in general, but
that's an issue for another time...)
All the tests pass in racket now, for me.
Racket appears to have a different notion of current directory than the
system does, so we need to tell it which directory we think we're in
when reading and writing bytevectors using the scheme file functions.
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)
Need to pass the LD_LIBRARY_PATH all the way through or racket doesn't
know where to look. I really don't know why it doesn't work to just set
it at the top level in the script, but it didn't (on my Mac, at least).
