This is for compiled evaluation at compile-time, for full normalisation. You can try it by setting the evaluation mode to scheme (that is, :set eval scheme at the REPL). It's certainly an order of magnitude faster than the standard evaluator, based on my playing around with it, although still quite a bit slower than compilation for various reasons, including:
* It has to evaluate under binders, and therefore deal with blocked symbols
* It has to maintain enough information to be able to read back a Term from the evaluated scheme object, which means retaining things like types and other metadata
* We can't do a lot of the optimisations we'd do for runtime evaluation particularly setting things up so we don't need to do arity checking
Also added a new option evaltiming (set with :set evaltiming) to display how long evaluation itself takes, which is handy for checking performance.
I also don't think we should aim to replace the standard evaluator, in general, at least not for a while, because that will involve rewriting a lot of things and working out how to make it work as Call By Name (which is clearly possible, but fiddly).
Still, it's going to be interesting to experiment with it! I think it will be a good idea to use it for elaborator reflection and type providers when we eventually get around to implementing them.
Original commit details:
* Add ability to evaluate open terms via Scheme
Still lots of polish and more formal testing to do here before we can
use it in practice, but you can still use ':scheme <term>' at the REPL
to evaluate an expression by compiling to scheme then reading back the
result.
Also added 'evaltiming' option at the REPL, which, when set, displays
how long normalisaton takes (doesn't count resugaring, just the
normalisation step).
* Add scheme evaluation mode
Different when evaluating everything, vs only evaluating visible things.
We want the latter when type checking, the former at the REPL.
* Bring support.rkt up to date
A couple of missing things required for interfacing with scheme objects
* More Scheme readback machinery
We need these things in the next version so that the next-but-one
version can have a scheme evaluator!
* Add top level interface to scheme based normaliser
Also check it's available - currently chez only - and revert to the
default slow normaliser if it's not.
* Bring Context up to date with changes in main
* Now need Idris 0.5.0 to build
* Add SNF type for scheme values
This will allow us to incrementally evaluate under lambdas, which will
be useful for elaborator reflection and type providers.
* Add Quote for scheme evaluator
So, we can now get a weak head normal form, and evaluate the scope of
a binder when we have an argument to plug in, or just quote back the
whole thing.
* Add new 'scheme' evaluator mode at the REPL
Replacing the temporary 'TmpScheme', this is a better way to try out the
scheme based evaluator
* Fix name generation for new UN format
* Add scheme evaluator support to Racket
* Add another scheme eval test
With metavariables this time
* evaltiming now times execution too
This was handy for finding out the difference between the scheme based
evaluator and compilation. Compilation was something like 20 times
faster in my little test, so that'd be about 4-500 times faster than the
standard evaluator. Ouch!
* Fix whitespace errors
* Error handling when trying to evaluate Scheme
Even though the `Comment` aspect is not (currently) supported
in the IDEMode, this is crucial to get proper highlighting in
Katla's LaTeX & HTML backends.
* Version increment to 0.5.1
This is to remove the requirement on Chez >9.5
* Disable -Xcheck-hases, at least for the moment
If we're going to have this as an option, we need to have a portable way
of finding a sha256sum command. At the moment, we might find a command,
but different versions accept different options. We should at least
allow setting it via an environment variable, and we certainly shouldn't
fail if running the command fails.
* Update bootstrap code ready for 0.5.1 release
* Abandon auto search on undefined name
These might arise from names in other modules that haven't been
imported. But it's going to be an error whatever, so give up straight
away. Fixes#1925
* Fix typo
* Fix test source
* Record possible cause when we can't solve a goal
Normally, it's just because we searched and failed. But maybe sometimes,
it's because there's an undefined name, in which case, we can include
this in the error message.
This is good to record because it means we don't abandon elaboration at
the wrong time! Say, if a search fails due to an undefined name, but it
was only in one branch of an ambiguous elaboration.
* Add necessary arguments for perf009 test
* Remove __collect_safe from bootstrap chez
We don't need this for bootstrapping, and it prevents building on older
Chez, so we can just remove it. Also added a note to the release
checklist.
* Update Release/CHECKLIST
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: memoryruins <memoryruinsmusic@gmail.com>
* Update version numbers and bootstrap scheme
* Use wall clock time for search timeouts
That was always the intention in any case, rather than the process time.
* Small fix for incremental compilation
In incremental mode we need to add the arity of a compiled definition to
the hash, because if that changes, we need to rebuild the dependencies
too to make sure the arity is correct at the call site
* Fix indentation in CHANGELOG
Instead of having UN & RF (& Hole in the near future & maybe even
more later e.g. operator names) we have a single UN constructor
that takes a UserName instead of a String.
UserName is (for now)
```idris
data UserName : Type where
Basic : String -> UserName -- default name constructor e.g. map
Field : String -> UserName -- field accessor e.g. .fst
Underscore : UserName -- no name e.g. _
```
This is extracted from the draft PR #1852 which is too big to easily
debug. Once this is working, I can go back to it.
* Add function that checks whether a file is a terminal device.
* support isTTY function for NodeJS backend.
* don't accidentally interpret 'false' string as truthy number
* less code duplication.
* Update strings.rst
For some reasons the code blocks which are not set as 'idris' are not displayed in the readthedocs rendering.
* Update overloadedlit.rst
* Update overloadedlit.rst
* Abandon ambiguity resolution on undefined name
This has finally annoyed me enough to do something about it. If we get a
"no such variable" error there's no point exploring other branches.
* Removes spaces from test file
One day I'll update the linter to ignore test files. We should really
accept literally anything as a possiblity for test files, even if
removing the spaces is tidier.
* Reset context before throwing in 'successful'
Although I don't think this is strictly necessary for a fatal error, we
should still for the sake of tidiness reset the state when backtracking.
* Move Context into its own file
Just the core definition - this is so that we have access to it in
Core.Core, for inclusion in error messages, to save normalisation of
terms in errors until we actually show them.
* Normalise errors on display, not when they arise
This can save a lot of time in ambiguity resolution if the errors are
complicated, because the errors might never be displayed if it's in an
abandoned branch.
This involves lifting 'Context' out of Core.Context, because we need to
store it in Error, which is needed by Core, which in turn is needed in
Core.Context.
Also moved a couple of test caes from ttimp to idris2, so that the
errors get rendered properly and won't need updating unnecessarily. In
fact all of the ttimp tests - which were just part of the initial
scaffolding - are probably now subsumed by the idris2 tests.
* Add new coverage001 test files
If they don't, we can't turn them into patterns to match on, and we end
up looping. Possibly we could throw a different and maybe more
informative error instead of just making an unmatchable pattern.
Fixes#1895
* Split Normalise into three files
Evaluation, Quoting, and Conversion checking are distinct steps, and I'm
about to add some variations to quoting so better to reorganise a bit.
* Add a Quote mode that limits size of result
Sometimes normalising an expression is a good idea because it makes
things smaler, and sometimes it isnt, because it doesn't. We can't tell
in advance which situation we're in, but we can try speculatively
normalising something. This is good for case types and hole types - we
generally want the normal form, but if that's expensive, we should stop.
So, quote is now able to give up if it passes a certain size threshold
for stuck applications. By experimentation, it seems that up to 10
doesn't hurt too much, but beyond that it's better not to normalise at
all.
* Add the new normalise files
