Instead of merely generating a locally unique name, use the existing
code for generating a new unique variable name in the unifier, which is
therefore globally unique.
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")
