Commit Graph

1913 Commits

Author SHA1 Message Date
Edwin Brady
c6f125b79c Fix tail calls in node back end
Authored by @stefan-hoeck
Stefan also says "Please note: The fix is quick and dirty. I plan to
open an new issue about the state of the JS backend soonish, since the
whole code requires some cleanup and documentation."
2021-05-14 15:19:30 +01:00
Edwin Brady
ba10b46054 Add missing 'commit' on backtrack
This means we can add things to the main context rather than the staging
context, if the 'branch' is always bracketed with a 'commit'. It doesn't
make a huge difference, but it is at least tidy!
2021-05-13 20:28:41 +01:00
Edwin Brady
1d762d4920 Print constructor labels correctly 2021-05-13 16:09:12 +01:00
Edwin Brady
75de88d8ec Add missing cases in hashing ConInfo 2021-05-11 11:42:15 +01:00
Edwin Brady
f21a495711 Merge github.com:idris-lang/Idris2 into tweak-cg 2021-05-11 11:37:12 +01:00
Edwin Brady
efaf290d88 Calculate whether an inlining is safe
It's safe if all top level arguments are used at most once, meaning that
there's no risk of duplication.
2021-05-11 11:29:01 +01:00
G. Allais
004cc45e9d
[ test ] cosmetic changes & retest capability (#1394)
* Banners for test pools
* Summary with the list of failing tests at the end
* Option to write the list of failing tests to a file
* Option to read the list of tests to run from a file
* Using these two latest features to add a new make target to rerun precisely the tests that failed last time
2021-05-11 09:46:21 +01:00
Matus Tejiscak
1d70a83fcd Mention Compiler.Separate in the CHANGELOG. 2021-05-11 09:45:01 +01:00
G. Allais
ab241213f3
[ breaking ] making toList part of Foldable (#1395) 2021-05-11 08:26:00 +01:00
Matúš Tejiščák
4de7b2133a
[ new ] Add chez-sep codegen (#1359)
Co-authored-by: Johann Rudloff <johann@sinyax.net>
2021-05-11 08:20:19 +01:00
Niklas Larsson
1db440d3cf
Merge pull request #1393 from melted/select_foreign
Choose foreign string based on priority
2021-05-10 15:22:34 +02:00
Stefan Höck
f028981e5a
[ fix #801 ] Use Number for up to 32 bit integers on JS backends (#1375) 2021-05-10 12:17:09 +01:00
Zoe Stafford
8a7aeca1b0
[ builtin ] O(1) natToInteger for any 'Nat'-like type (#1363) 2021-05-10 12:14:19 +01:00
Guillaume ALLAIS
08d61d70c4 [ fix #1370 ] use the lambda's type for eta-expansion 2021-05-10 12:13:29 +01:00
Niklas Larsson
53094e3027 Choose foreign string based on priority
Instead of taking the first applicable string, the backends submit an
ordered list of preferred prefixes and get the first match.
2021-05-10 13:00:57 +02:00
alissa-tung
50481038a3 [ contrib ] add 2021-05-10 11:54:23 +01:00
Zoe Stafford
25ae664ef6
[ fix #1378 ] Collect constructors after inlining (#1380) 2021-05-10 11:19:18 +01:00
Denis Buzdalov
8038f0a0f9 [ refactoring ] Tiny changes following up the idris-lang/Idris2#830
Some zeroes in signatures, one simpler implementation and formatting.
2021-05-10 09:07:36 +01:00
Ohad Kammar
e58bcfc7ef
Semantic highlighting (#1335)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-05-10 09:05:43 +01:00
Edwin Brady
251d77b92d Swap 'False' and 'True' constructors
It has always bothered me that 'False' got mapped to tag 1 and 'True'
got mapped to tag 0. This doesn't change much in practice (except that
perhaps a code generator might notice some useful things in intToBool)
but I'm changing it now anyway. Also added a couple of inlinings of
boolean operations.
2021-05-09 20:08:38 +01:00
Edwin Brady
c54c1a6e97 Add some inlines
We should really get these automatically, but until we do, add the
flags. Chez seems to spot these anyway, but again it makes the generated
code easier to look at, and it removes some needless abstraction over
interfaces at runtime.
2021-05-09 17:31:44 +01:00
Edwin Brady
e8eab6d763 Flag records and option types
This saves a small amount of allocation, especially since we never
actually look at the tag in a record. We can use null? for Nothing just
like for Nil.
2021-05-09 16:49:59 +01:00
Edwin Brady
39f844dae9 Remove some unnecessary lets from generated scheme
Chez probably already does this for us, but it's tidier and makes the
output smaller and easier to read (and debug, when necessary).
2021-05-09 14:50:28 +01:00
Edwin Brady
416cf6af3e
Merge pull request #1390 from edwinb/caseofcase
Some optimisations on case compilation
2021-05-09 11:49:24 +01:00
Edwin Brady
53989f512f Convert all enumerations to integers at runtime
We were just doing Bool/Ordering but now generalised to everything where
all the consructors are nullary after erasure
2021-05-09 02:27:38 +01:00
Edwin Brady
fafa76c55c Generalise NIL/CONS to all list shaped things
Also pairs turn into CONS, because we don't need to look at the tag if
there's only one constructor.
2021-05-09 01:43:59 +01:00
Edwin Brady
4389224694 Merge github.com:idris-lang/Idris2 into caseofcase 2021-05-08 18:19:21 +01:00
André Videla
9b99aba992
Merge pull request #1386 from Russoul/prelude-interface-constructors
[prelude] Add explicit constructor to every interface
2021-05-08 17:05:56 +00:00
Edwin Brady
251ba812d6 Keep linter happy 2021-05-08 15:52:47 +01:00
Edwin Brady
66930113bd Compile lists as scheme lists
This also involves adding a flag to constructors and case alternatives
in CExp which say whether it's a NIL or CONS. Currently, we only do this
for Prelude.List, which already has an effect, but soon I'll extend this
to work for all list-shaped things and rather than being hard coded. We
could also imagine spotting other shapes (enumerations especially) for
code generators to spot as they see fit.

This will require code generators to be fixed to recognise the new
ConInfo flag, but you can just ignore it.

Bootstrap code also updated, because we don't currently have a way of
having separate support.ss/rkt for the bootstrap and normal builds!
2021-05-08 15:42:51 +01:00
Ruslan Feizerakhmanov
51184c156d [doc] Interface constructors 2021-05-08 11:36:12 +03:00
Edwin Brady
196194c73f Add case-of-case transform
This lifts case blocks out of the scrutinee of a case expression, in
some limited but useful circumstances.
2021-05-07 10:17:51 +01:00
Ruslan Feizerakhmanov
5993233057 [test] Update the test that prints constructor names 2021-05-06 19:48:12 +03:00
Ruslan Feizerakhmanov
d203597eb9 Merge branch 'master' of https://github.com/idris-lang/Idris2 2021-05-06 19:30:50 +03:00
Ruslan Feizerakhmanov
af7edd72bb [prelude] Add explicit constructor to every interface 2021-05-06 18:32:51 +03:00
Johann Rudloff
4b7d85653a [ tests ] Add tests for :doc for records and single-constructor type 2021-05-06 14:38:55 +01:00
Johann Rudloff
d8891bf7b9 [ docs ] Show constructor for records (REPL and HTML) 2021-05-06 14:38:55 +01:00
Johann Rudloff
190932fd01 [ docs ] Remove unnecessary newlines in HTML declaration lists
As a relict of the REPL output, several `<br>` tags where introduced,
where they are not needed or even permitted. This led to some spacing
issues (sometimes the docstring was closer to the next term than to the
one above that it actually described).

To counter the removed forced newlines, some extra margin is added below
each declaration.

As a side-effect, this also makes the W3 "Nu Html Checker" happy.
2021-05-06 14:38:55 +01:00
Johann Rudloff
0ab5fe2535 [ docs ] Correctly wrap data constructor docstrings with DocStringBody annotation 2021-05-06 14:38:55 +01:00
Guillaume ALLAIS
7c3960ab52 [ fix ] emacs' terminal is "dumb"
emacs sets the TERM variable to "dumb" and expects not to have to
handle any ANSI escape codes as a consequence. We need to patch the
renderer to unannotate the Doc in this situation.
2021-05-05 20:26:02 +01:00
Johann Rudloff
62519c5352 Allow --directive command line flag combined with package options 2021-05-05 18:55:55 +01:00
Stefan Höck
6cdf05f1ec
[ new ] Add Int(8/16/32/64) (#1352)
This adds new `Int8`, `Int16`, `Int32` and `Int64` data types
to the compiler, thus working towards properly specified integer
types as discussed in #1048.

In addition, the following changes / corrections are made:

* Support casts from `Char`, `String`, and `Double` to all integer
  types (and back). This fixes #1270.
* Make sure that all casts to limited-precision integers are properly
  bounds checked (this was not the case so far for casts from `String`
  and `Double` to `Int`)
* Add a thorough set of tests to make sure all bounds checks work
  correctly for all supported casts and arithmetic operations
2021-05-04 08:22:06 +01:00
Edwin Brady
e972a23126
Merge pull request #1371 from edwinb/eraseargs
Erasing more things
2021-05-03 16:46:27 +01:00
Edwin Brady
71b401d3de Update tests
Well that was clever. I updated my tests locally and forgot to include
them in the commit...
2021-05-03 15:13:45 +01:00
Edwin Brady
09c4b6cc03 Recalculate call graph after inlining
This means we can eliminate unused definitions from the generated code.
As usual, this doesn't make the generated code any faster, or the chez
compilation, but it's still good for tidiness and it does make the
generated scheme smaller.
2021-05-03 14:24:03 +01:00
Edwin Brady
73d374e435 Properly erase 0 quantity arguments
Don't just have a placeholder. While this doesn't have a huge effect (if
any) on performance, it does generate smaller output for Chez to
process, and is tidier. Perhaps it's good for other back ends too, ones
that don't optimise as much as Chez does.

Only doing named functions, not higher order functions. HOFs may be
worth doing too, if we can, since this could remove lambdas and make
fewer closures.

The increment in TTC Version is necessary because otherwise there could
be inconsistencies between libraries and clients erasure properties.
2021-05-03 14:18:01 +01:00
Guillaume ALLAIS
32f42e702a [ fix #1366 ] NType is not an NTCon 2021-05-03 13:52:01 +01:00
Johann Rudloff
0490b3de98 [ docs ] Fix operators and docstrings not being HTML-escaped 2021-05-03 11:44:42 +01:00
Johann Rudloff
da51c1c2fe [ docs ] Fix #1367: Missing spaces in type signatures in WebKit-based browsers
WebKit seems to throw away any sequence of spaces between inline tags.
All affected places I found could be fixed by replacing single space
characters with the character U+2002 ("EN Space"), which means
almost the same thing as "normal space" (i.e. it breaks/wraps text and
has approximately the same width) but is not discarded by WebKit when
parsing the document.

If this should come up in a different place, a more thorough solution
might be needed (e.g. modifying `htmlEscape` to replace all spaces).
2021-05-03 11:44:42 +01:00
Johann Rudloff
182a3caa3e [ docs ] Fix strange indentation on WebKit-based browsers (partial fix for #1367) 2021-05-03 11:44:42 +01:00