idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity
2,177 Commits 5 Branches 9 Tags 122 MiB
afaf416673
Commit Graph

2177 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Denis Buzdalov
0392b49c63 [ doc ] Update the test-lib's readme according to the current state 2021-05-14 11:46:11 +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
Zoe Stafford
7e520994fd
[ fix ] missing log option (#1411) 2021-05-13 20:23:31 +01:00
Zoe Stafford
7fe8c42116
[ builtin ] O(1) integerToNat for any 'Nat'-like type (#1403) 2021-05-13 18:44:24 +01:00
Johann Rudloff
2477d060a8 Use sysctl instead of nproc to get number of processors on FreeBSD 
On FreeBSD `nproc` is not available in a standard installation, so the
equivalent `sysctl -n hw.ncpu` is used.
 2021-05-13 18:27:57 +01:00
Johann Rudloff
b9e95d5d8d Do not explicitly load libc on FreeBSD 
On FreeBSD, the versionless `libc.so` file is a (text-based) linker
script and can not be loaded dynamically at runtime. Instead of
hardcoding the libc version "7" for FreeBSD we can just skip the load
completely, since libc is already implicitly loaded by the Chez runtime.
 2021-05-13 18:27:57 +01:00
Johann Rudloff
664a7616b1 Remove path and version from Racket libc FFI definer 
According to [1], Racket recommends specifying `#f` as "library path"
when the goal is to access functions of the C runtime.

This enables using the Racket backend on systems where libc is not
always version "6" (e.g. on FreeBSD it's "7").

[1]: https://docs.racket-lang.org/foreign/Loading_Foreign_Libraries.html#%28def._%28%28lib._ffi%2Funsafe..rkt%29._ffi-lib%29%29
 2021-05-13 18:27:57 +01:00
Guillaume ALLAIS
210026061d [ fix ] Handle ambiguous DPair/MkDPair 2021-05-13 18:26:06 +01:00
stefan-hoeck
1a6c8eeee3 [ fix ] support all log level prefixes 2021-05-13 18:04:20 +01:00
stefan-hoeck
c798f6dbbd [ fix ] auto-complete known log topics 2021-05-13 18:04:20 +01:00
Guillaume ALLAIS
ecfa1f5bb1 [ debug ] adding existing log levels to autocompletion 2021-05-13 18:04:20 +01:00
Guillaume ALLAIS
dece43117f [ refactor ] minor changes 2021-05-13 18:04:20 +01:00
stefan-hoeck
2a57f1ca33 [ doc ] instructions for activating tab completion 2021-05-13 18:04:20 +01:00
stefan-hoeck
8d4c95512c [ new ] tab auto-completion in bash-like shells 2021-05-13 18:04:20 +01:00
Denis Buzdalov
5b246eda53 [ totality ] Make Language.Reflection modules have %default total 2021-05-13 17:38:31 +01:00
Edwin Brady
1d762d4920 Print constructor labels correctly 2021-05-13 16:09:12 +01:00
Stefan Höck
364eaff6ac
[ towards #1124 ] Statically enforced logging (#1402) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-05-12 11:57:49 +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