idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 22:51:51 +03:00
Code Issues Projects Releases Wiki Activity
2,087 Commits 6 Branches 9 Tags 116 MiB
a15136b3b2
Commit Graph

2087 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
a15136b3b2
Merge pull request #1590 from edwinb/eval-updates-take2 
Some evaluator tidying, CBV evaluation (second attempt)
 2021-06-21 14:10:43 +01:00
Edwin Brady
ab2012a7dc Small change in output of reg042 
No idea what happened there. Maybe a minor change in the input? Anyway,
this updates it as it should be.
 2021-06-21 13:07:26 +01:00
Edwin Brady
e35930a2aa Change reg042 to look at compiler output 2021-06-21 12:41:55 +01:00
Matt Smith
95710c3a29 Add chezscheme binary to search path 
The Gentoo Chez package and some versions of the Ubuntu package
install Chez scheme as `/usr/bin/chezscheme' which requires manually
setting the CHEZ environment variable.  Adding it to the search path
makes it easier for these users.

Closes: https://github.com/idris-lang/Idris2/issues/666
 2021-06-21 11:20:12 +01:00
Edwin Brady
37f8c2c58f Merge github.com:idris-lang/Idris2 into eval-updates 2021-06-20 21:35:56 +01:00
Robert Wright
a8264f8f05 Add ability to extend RefC backend to create further backends 2021-06-18 16:59:35 +01:00
Fabián Heredia Montiel
657699a866
[doc] Add missing entries and refactor CHANGELOG.md (#1566) 2021-06-18 16:45:00 +01:00
Tim Engler
68c6fe222c
[ Fix #1577 ] Actually use natMinus hack (#1578) 
And also make sure that the output is truncated to 0.

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-18 11:50:54 +01:00
G. Allais
f3177e0cc1
[ fix ] print postfix projections... postfix (#1557) 2021-06-18 00:00:51 +01:00
CodingCellist
55f8bc3b90
Improve case-splitting formatting to not introduce new whitespace; add a bit of comments+docs. (#1553) 2021-06-17 16:48:59 +01:00
Nick Drozd
3e3a4e1b78
Use truncated case notation (#1562) 2021-06-17 15:52:19 +01:00
Stefan Höck
c04835c436
[ cleanup ] Reuse Tarjan's algorithm in JS backend and some other cleanups (#1504) 2021-06-17 12:43:10 +01:00
Alissa Tung
41c3fd2632
[docs] ind-ind ind-rec rec-rec in style of fwddecl (#1558) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-06-16 16:20:11 +01:00
Fabián Heredia Montiel
e0e8403317
[ new ] detect changes using sha256 rather than timestamps (#1535) 
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing
a file is enough to get it recompiled.

Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
 2021-06-16 16:16:58 +01:00
Nick Drozd
0db136d168
Hoist some pures (#1556) 2021-06-16 15:22:52 +01:00
Nick Drozd
ec438760d9
Simplify some lambdas (#1561) 2021-06-16 15:22:30 +01:00
Edwin Brady
9fbdf5655e Add CBV mode to the evaluator 
I'm not sure how useful this is going to be, but I set it as the default
for evaluation at the REPL, since it can save duplicating work.

It's not a good choice for evaluation during type checking, since we
want to avoid evaluation when we don't need it. Also when we resume
suspended unification problems, the context may be different due to
solved metavariables, so even if we evaluate early we might still have
to evaluate again.
 2021-06-16 13:50:48 +01:00
Edwin Brady
ff9725bbb1 Tidy up applyToStack/continueNF 
It's best if they don't use 'quote' (which actually is a potential
problem anyway, if quotes somehow end up nested).

applyToStack actually only worked properly for NTCon/NDCon/NPrim,
although in practice that was fine since it was only ever called in
those contexts. This fixes it so it properly continues evaluation, which
means we have a chance of caching results in more cases.
 2021-06-16 11:30:15 +01:00
Edwin Brady
a3a9b5c6a3 Merge github.com:idris-lang/Idris2 2021-06-15 23:21:19 +01:00
Fabián Heredia Montiel
a28bc65544
Fix deadlocks [Rebased, Squashed] (#1536) 
Co-authored-by: Arnaud Bailly <arnaud.oqube@gmail.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Fabián Heredia Montiel <fabianhjr@protonmail.com>
Co-authored-by: Ruslan Feizerakhmanov <me@russoul.me>
 2021-06-15 14:31:31 +01:00
Kamil Shakirov
7692de67aa Allow underscores in integer literals to aid readability 2021-06-15 13:00:53 +01:00
Nick Drozd
488b4709f4
Use map for some maybes (#1548) 2021-06-14 17:52:43 +01:00
Fabián Heredia Montiel
757f41fbbe [test] Add preformance test of Fin/Vect 
Closes idris-lang/Idris2#16
 2021-06-14 17:28:58 +01:00
claymager
b946ec0277
[ fix ] Create library dir if necessary (#1300) 2021-06-14 16:12:46 +01:00
CodingCellist
ac31e17636
[ refactor ] Right-align padded numbers. (#1554) 2021-06-14 15:29:20 +01:00
Martin Molzer
a91b45daf0 use socketaddr_storage in getsockname 2021-06-14 15:21:46 +01:00
Robert Wright
e9b42cc55e Guarantee Ref C Buffer 0 initialization 2021-06-14 15:06:44 +01:00
Robert Wright
1875f62248 Remove freeBuffer function 
Each backend is now responsible for freeing Buffers in the same way as other objects
 2021-06-14 15:06:44 +01:00
Robert Wright
195e690ddc Fix RefC Buffer getInt function to work with large values 2021-06-14 15:06:44 +01:00
Robert Wright
c6a5827319 Add RefC readBufferData/writeBufferData support 2021-06-14 15:06:44 +01:00
Robert Wright
d202139171 Distinguish common C and RefC Buffer functions 2021-06-14 15:06:44 +01:00
Robert Wright
c63f25dac2 Distinguish common C and RefC FFI calls 2021-06-14 15:06:44 +01:00
Robert Wright
85e4df8004 Add filenames to Golden Test missing file error reporting 2021-06-14 12:56:39 +01:00
Mathew Polzin
0209cee41a include the other definition of drop because both are quite useful. 2021-06-14 11:44:38 +01:00
Mathew Polzin
1133658e18 Add missing unlock in signal handling C code. 2021-06-14 11:44:38 +01:00
Mathew Polzin
bdd8f4157b Add drop for Vect. 2021-06-14 11:44:38 +01:00
Nick Drozd
4a0a5759b8
Return Maybe from strengthen (#1540) 
Co-authored-by: Fabián Heredia Montiel <303897+fabianhjr@users.noreply.github.com>
 2021-06-14 10:59:49 +01:00
André Videla
161ea5d50a
Merge pull request #1521 from LibreCybernetics/add-totality-annotatations 
Add totality annotations to `src` and `libs/{prelude, base}`
 2021-06-13 19:51:48 +00:00
André Videla
508ef8d0ce
Merge pull request #1527 from LibreCybernetics/color-tests 
Add color to tests
 2021-06-13 16:41:18 +00:00
Fabián Heredia Montiel
4c99537062 Add color to tests 2021-06-13 10:36:30 -05:00
Edwin Brady
40fa9b43a7
Merge pull request #1547 from edwinb/fix1510 
A couple of fixes
 2021-06-13 14:51:07 +01:00
Edwin Brady
fda76b841f Merge github.com:idris-lang/Idris2 2021-06-13 14:05:08 +01:00
Edwin Brady
97ee3d4cd3 Check LHS arguments are polymorphic enough 
We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes #1510, and also now gets the error location
right as a bonus!
 2021-06-13 13:31:40 +01:00
Denis Buzdalov
bf0985602f [ totality ] More %default total stuff 2021-06-12 21:06:08 -05:00
Fabián Heredia Montiel
dad4dcdaf8 Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
André Videla
42d4c36833
Merge pull request #1522 from LibreCybernetics/cleanup-src-libraries 
Cleanup src libraries (Remove `Libraries.Data.Bool.Extra` and half `Libraries.Data.List1`) since they have been included since v0.3.0
 2021-06-12 21:54:34 +00:00
André Videla
9b94108b7b
Merge pull request #1542 from andorp/andorp/contributors-wanted 
Contributions wanted section in README.
 2021-06-12 20:39:33 +00:00
André Videla
ba92a82c78
Contributors -> Contributions 2021-06-12 21:38:14 +01:00
Andor Penzes
012d7f80ce [ README ] Contributors wanted. 2021-06-12 20:42:00 +01:00
Edwin Brady
19cb2681be Only fully normalise fromInteger on LHS 
This reduces surprising undefined name errors on the RHS, as noted in
issue #1541
 2021-06-12 14:23:25 +01:00