Commit Graph

1891 Commits

Author SHA1 Message Date
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
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
Edwin Brady
5bbcb29a38
Merge pull request #1362 from edwinb/makedocs
Make documentation from Makefile
2021-05-01 18:36:52 +01:00
Edwin Brady
9e082730c2 Update test output
Some merges have made the output of tests change (due to internal
changes). This brings them up to date.
2021-05-01 17:37:38 +01:00
Edwin Brady
587f73a256 Make documentation from Makefile
The documentation is now also linked from
https://www.idris-lang.org/pages/documentation.html
and https://www.idris-lang.org/pages/idris-2-documentation.html
2021-05-01 17:09:25 +01:00
Edwin Brady
ad78f8210a
Merge pull request #903 from cypheon/mkdoc
WIP: Generate documentation from source code (aka `--mkdoc` support)
2021-05-01 16:26:19 +01:00
Edwin Brady
5df243748c
Merge pull request #1360 from RaoulHC/rebindable-do-syntax-docs
Update docs to reflect usage of >> in do syntax
2021-05-01 16:23:14 +01:00
Edwin Brady
8d3eb3eaea
Merge pull request #1336 from cypheon/lambdalift-opt
Lambdalift optimisation: drop unused variables from outer scopes
2021-05-01 16:22:32 +01:00
Edwin Brady
d6d68ff09b
Merge pull request #1195 from buzden/some-funs-to-lazy-list
[ contrib ] Some functions for lazy list + fix for `foldlM`
2021-05-01 16:18:24 +01:00
Raoul Hidalgo Charman
2c8f2483de Update docs to reflect usage of >> in do syntax 2021-05-01 15:18:49 +01:00
Edwin Brady
93f4092e94
Merge pull request #1357 from edwinb/optimising
A couple of optimisations
2021-04-30 18:56:32 +01:00
Edwin Brady
3bd1ad222e Replace an old log
This comes up in a test, and I don't think it affects evaluation
performance while typechecking, since we compute 'redok2' there.
2021-04-30 16:49:23 +01:00
Edwin Brady
ee9989ba09 Reduce logging overhead
Checking the log categories isn't cheap because it involves parsing a
string. So, record whether we've ever set a log level. If we haven't,
there's no point in checking the string. This reduces overhead and saves
a few seconds in typechecking the Idris code base - also means we don't
have to worry so much about adding more logging if we feel we need it!
2021-04-30 12:41:46 +01:00
Edwin Brady
7f7b11ed54 Use transforms for fastPack/fastUnpack
We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.

Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
2021-04-29 23:17:29 +01:00
Edwin Brady
f966c99a5a
Merge pull request #1355 from edwinb/profileflag
Add --profile flag
2021-04-29 16:30:27 +01:00
Edwin Brady
6d37471ccc Add --profile flag
If set, when compiling this generates an executable which generates
profiling data. Currently supported by Racket and Chez, other backends
silently ignore it.
2021-04-29 15:18:59 +01:00
Edwin Brady
90ec19f053
Merge pull request #1354 from edwinb/casetransform
Add case+lambda transformation
2021-04-29 14:59:11 +01:00
Johann Rudloff
18f9c5484d [ refactor ] Pass through Used vars instead of creating and merging 2021-04-29 15:41:23 +02:00
Edwin Brady
3bb4333ac3 Fix whitespace error 2021-04-29 13:47:31 +01:00
Edwin Brady
c3e5689a62 Add case+lambda transformation
If all branches in a case block are a lambda, lift the lambda out. In
many cases, this can save creating a closure then evaluating it
immediately, because the function is already applied to the extra
argument.

This happens in particular with IO based code, where the extra argument
is the world token. One place where this transformation has a big effect
is 'evalRef' so the evaluator is now a bit faster (about 20% on the
small benchmark I tried it on - but no guarantees that's going to happen
on other examples!)
2021-04-29 13:44:13 +01:00
Johann Rudloff
8d21a292d0 Add Text.PrettyPrint.Prettyprinter.Render.HTML to contrib as well 2021-04-29 13:49:04 +02:00
Johann Rudloff
9591b147a4 [ cleanup ] Remove unused helper function 2021-04-29 13:41:34 +02:00
Johann Rudloff
f656b97928 [ refactor ] Move all HTML-related code out of the Idris.Package module 2021-04-29 11:56:47 +02:00
Johann Rudloff
8012736e83 [ fix ] Add new module to the ipkg file 2021-04-29 11:29:37 +02:00