From here on, this repo is intended only as a bootstrapping step for the
self hosted Idris 2. It will - as long as possible - be kept up to date
enough that it can build Idris 2, but won't be maintained beyond that.
Back ends can still shortcut these and use their own primitives, but
doing things this way gives consistent behaviour between the simple IO
primitives and file IO, and allow us to use stdin/stdout consistently
(e.g. to flush stdout).
This also fixes the behaviour of 'replWith' to be consistent with the
Idris 1 version.
This removes the need for some external primitives, and allows the
details to be shared between all the backends (plus we don't have to do
things a certain way just because Scheme chooses to)
A big cost in IO heavy programs is io_bind, and we can often inline it
away and turn it into just sequencing operations. Things have to be
lined up right to do that though - ideally, case inlining and the
newtype optimisation will know just a little bit more to be able to do
it automatically, but for now, the inliner treats io_bind as a special
case.
Also do another round of inlining, since lots more things can become
inlinable (io_bind especially, becoming fully applied to the %World)
after the first pass.
It's slightly different wrt to file reading and writing, and now
requires the created buffer to be explicitly freed (since unlike Idris 1
the run time can't be told to manage C values) but this makes the buffer
code more portable by not requiring it to run via scheme.
Performance appears more or less the same as before.
Need to note we can't add a laziness coercion under 'unifyInvertible',
which is where we unify things under metavariables which are known to
stand for constructor forms. Fixes#360
Solving later arguments first means that they can refer to solutions of
earlier arguments. This isn't really the best solution for ensuring that
metavariables refer to things defined earlier, but it helps, and it does
fix#304.
Instead of the previous unreliable hack, actually look for occurrences
of the solved metavariable. Block if there are any, and fail if there
are any under a constructor. I had expected this to hurt performance
quite a bit, but it seems it doesn't.
This was prompted by #304, which is now partly fixed, but there's still
a refinement to unification needed to fix it fully (and at least it
doesn't segfault due to the cycle now!)
A bug found via the very handy, but occasionally bad for performance so
off by default, --debug-elab-check. The multiplicity of a lambda type
needs to be checked against the expected multiplicity, not the given
multiplicity. Oops!
If you have any (\0 x => e) or similar, you may find you need to fix a
type error after this update...
At least as long as the number is small enough (currently set to < 100).
This is because it can open up further evaluation opportunities when
typechecking, and can make the term we're working with smaller - it also
makes display a bit neater.
Overall this makes some pathological cases of terrible performance much
better, without hurting anything else.
While Bird Style literate mode is useful, it does not lend itself well
to more modern markdown-like notations such as Org-Mode and CommonMark.
This commit extends Idris2's existing literate mode to recognise both
'visible' and 'invisible' code blocks and lines in predefined markdown
styles.
The styles and their elements are:
+ Bird Style :: `>` denotes a visible code line, `<` a hidden code
line.
+ OrgMode :: Org Mode source blocks for idris are recognised as
visible code blocks, and comment blocks are invisible
code blocks. Invisible code lines are denoted with
`#+IDRIS:`.
+ CommonMark :: Only code blocks denoted by standard code blocks
labelled as idris are recognised.
For backwards compatibility, we recognise literate modes by file
extension:
+ Bird Style :: `.lidr`
+ OrgMode :: `.org`
+ CommonMark :: `.md`
In future we should add support for literate `LaTeX` files, and more
intelligent processing of literate documents using a pandoc like
library in Idris such as: [Edda](https://github.com/jfdm/edda).
