(Which was commented out anyway)
Three scheme back ends is enough to maintain, and Gambit does the same
job as chicken (fast startup of the interpreter, generating via C) but
seems to deal with the code Idris generates better.
ANF, in which everything is applied to variables only, and VMCode, in
which everything is reduced to a list of assignments.
I don't plan to add a defunctionalisation step. I've tested with with a
quick hack C backend, though I don't intend to commit that (not here at
least) because even though it basically works, it's Very Slow.
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).
It's not actually used as part of any compilation pipeline yet, and I've
only tested it by eyeballing the output, but it'll be useful soon, and
it's good for it to be available to any new back ends that might need
it. It will need some optimisation.
- Add support for .lidr files.
- Add new Parse Error for Literate fails.
- Add support for Case Split.
- Add support for Add Clause.
- Add support for Add Lemma.
- Add tests.
This has two main advantages: firstly, it actually makes the build slightly
faster and less memory intensive, because Idris doesn't fork a new
process and eat all the memory! Secondly, it means we can build a
distribution with the C file, for building on machines which don't have
Idris 1 available.
Also includes a script for building such a distribution.
I expect someone who is better a writing Makefiles than me can tidy this
up. There are almost certainly problems on Windows too - please help if
you can!
There are new Make targets 'all-fromc' and 'install-fromc' which don't
require building from Idris source, so that we can build with no Idris 1
available.
A small consequence: make install-exec no longer builds the idris2
executable, just installs it.
These can give valuable information, but since they're not well typed,
we have to rebuild as close an approximation as we can before passing it
to the case tree compiler. We can do this in a type-directed way, but
ignoring whether any of the arguments are convertible, and not trying to
solve any of the implicits. If this fails, it doesn't use the impossible
case, otherwise it uses it to find the missing cases in the resulting
case tree.
This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
When writing to ttc, need to take the length in bytes rather than the
length in characters. Also need to write to scheme in the appropriate
format for each scheme system.
While we're at it, Idris 1 supports unicode identifiers (although we
don't encourage it :)) so this allows any characeter >127 in an
identifier.
This could allow us to actually erase (rather than compile with nil)
although experiments show that has no impact on performance. It is
useful to see, though, and other back ends may benefit.
Since lookup up a binding can be expensive in a big environment, and we
only need to reduce it if it turns out to be a let, caching it can be a
noticeable win
With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).
