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.
A %macro must always be fully applied. Whenever the elaborator
encounters a %macro application (except in a function LHS) it evaluates
the application and sends the result to %runElab. So:
%macro
foo : args -> Elab TT
...
def = foo a b c
is equivalent to
foo : args -> Elab TT
...
def = %runElab foo a b c
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'.
It seems relevant to all BSD systems.
In xcode the option -Wno-error-implicit-function-declaration is enabled. So the following error occured:
Idris2/support/c/idris_file.c:76:13: Missing '#include <sys/time.h>'; declaration of 'select' must be imported from module 'Darwin.POSIX.sys.time' before it is required
I hope it won't break anything on linux.
The bootstrap version has an occasional bug with as patterns, which is
tripped by elabScript. This works around it.
(I'd rather do this than update the Scheme, since Idris2-boot will still
work this way!)
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)
This makes vim mode work again.
I don't know a good way to test this, since it involves dealing with
absolute paths. If anyone has the bash skills to get this working in a
pkg test, please do...
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")
building Chez Scheme locally from source and
improve formatting of first paragraphs
```
Compiling idris2_app/idris2-boot.ss with output to
idris2_app/idris2-boot.so
Exception: attempt to reference unbound identifier
make-thread-parameter at line 171, char 30 of idris2_app/idris2-boot.ss
```
As patterns weren't getting propagated to local definitions, due to a
combination of being stored as let bindings and being part of a pattern
scrutinee. The solution removes the computation behaviour, but that is
consistent with the way let works everywhere else.
(If we do as patterns as let bindings, the way case and locals elaborate
mean that the value gets recomputed. Fixing this would require changing
the way the core works, and I'm not going to do that for a while.)
