I was getting a stack overflow on the tailrec002 test, caused by this
primitive being recursive. I've made it iterative. I'm no JS expert but
I've tested its behaviour against the old version.
* [ fix ] Fix returned status of the `system` function
* [ re #238 ] Fix program error condition of `git diff` call in `Golden`
According to documentation, not only negative exit code means error
Previously, the RefC files were located in IDRIS2_PREFIX. This is
decoupled to allow users to change the prefix (for ad-hoc library
install locations, for example).
* Fix casts in scheme evaluator
We really need test cases for all the primitives before we can use this
evaluator properly. Also test cases that run inside an environment,
which are a bit harder to construct.
* Add the cast fixes to racket support code
* More racket compile time evaluation fixes
We had the chez version of some primtives in the ct-support file. We
need a full set of tests for the primitives here too...
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
* 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.
This is step 0 in a plan to use the scheme evaluator to evaluate Idris
expressions at compile time. As a proof of concept, I've got this
working for a toy language here: https://github.com/edwinb/SchemeEval
We won't be able to do anything interesting with this in Idris itself
until the next release because it involves updating the bootstrap code
and adding the ability to pass 'Integer' to foreign calls, which really
should have been allowed anyway since it's for a backend to decide what
it can cope with, not Idris itself.
* add `nextDirEntry` which returns `Maybe String`, so `Nothing` on
the end of directory unlike `dirEntry` which returns unspecified error
on the end of directory
* `dirEntry` is deprecated now, but not removed because compiler depends on it
* native implementation of `dirEntry` is patched to explicitly reset `errno`
before the `readdir` call: without it end of directory and error were
indistinguishable
* test added
Operating system counter stores signals as flag set without counter.
So sending two signals to a process may result to one or two signal
handler invocation. Queueing signals inside Idris could give users
false sense of signals being are queue, while they are not.
In particular, test for signal could not work reliably for that
reason.
Also, practically we usually don't need have more than once signal
event.
This is follow-up to #1660. CC @mattpolzin
To be able to use `C` functions for both Scheme and RefC: it was
not possible for `Buffer` before this PR.
As an example, `writeBufferData` and `readBufferData` functions are
removed: generic C backend implementations are used instead.
```
IDRIS2_VERIFY(cond, message_format, ...)
```
When condition is false, crash.
Used in native functions where correct error handling is hard or
not impossible.
For example, `malloc` rarely fails, but if it fails, better crash
with clear error message than spend time debugging null pointer
dereference.
* add `strerror` function
* move `getErrno` to `System.Errno`
* use `strerror` in `Show FileError`
* on node there's no access to `strerror`, so `strerror` just converts the number to string
Pragma once is supported by all compilers for the last ten years.
Better use it instead of include guards (which use different styles
in different files).
Support for simple signal handling was added in
a0a417240e. This commit also adds the
`_simple_handler` function. It seems to me that this function is
intended as a helper function which should only be visible in
`idris_signal.c`, it is not used outside this file. For this purpose it
is probably also marked as inline. However, the inline keyword does not
require the compiler to actually inline the function. As such, the
`_simple_handler` symbol may still be exported if the compiler doesn't
inline the function.
On my system this seems to be the case and causes the following error
during compilation of idris2:
Exception: (while loading libidris2_support.so) Error relocating Idris2-0.4.0/build/exec/idris2_app/libidris2_support.so: _simple_handler: symbol not found
By marking the `_simple_handler` function as `static inline` it is
ensured that the symbol is not exported, thereby preventing the
relocation error.
To be able to eventually refactor/extend `system` function: to be
able to specify a directory, environment variables, specify arguments
as array etc. Ideally it should be something like Rust
[`std::process::Command`](https://doc.rust-lang.org/std/process/struct.Command.html).
