This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
When writing to ttc, need to take the length in bytes rather than the
length in characters. Also need to write to scheme in the appropriate
format for each scheme system.
While we're at it, Idris 1 supports unicode identifiers (although we
don't encourage it :)) so this allows any characeter >127 in an
identifier.
This could allow us to actually erase (rather than compile with nil)
although experiments show that has no impact on performance. It is
useful to see, though, and other back ends may benefit.
Since lookup up a binding can be expensive in a big environment, and we
only need to reduce it if it turns out to be a let, caching it can be a
noticeable win
With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).
