idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Code Issues Projects Releases Wiki Activity
2,322 Commits 6 Branches 9 Tags 115 MiB
ee063a5412
Commit Graph

724 Commits

Author SHA1 Message Date
Stiopa Koltsov
5a351f4e7e Accept HasIO in onCollect functions 
Since most functions work with `HasIO`, it is more convenient to
accept `HasIO` in `onCollect` and `onCollectAny`.
 2021-07-17 14:42:34 +01:00
Alex Humphreys
f195aed2cd [ Test ] allow 'N' as an acceptable response 
Situation I just ran into that I found confusing:
```
Golden value differs from actual value.
Accept actual value as new golden value? [y/N]
N
Invalid answer.
```
 2021-07-17 13:29:13 +01:00
Zoe Stafford
0fec867583 [ fix ] Name in Language.Reflection.TT 
This was different to `Name` in `Core.Name`
Specifically `CaseBlock` and `WithBlock` had an `Int` instead of a `String`
 2021-07-16 20:05:49 +01:00
Edwin Brady
d2af6e5027 Export throw and catch again in App 
Fixes #1706
 2021-07-16 11:42:24 +01:00
Edwin Brady
66217b6fa6
Merge branch 'master' into refc-buffer 2021-07-16 09:44:40 +01:00
Edwin Brady
050abe663e
Merge pull request #1638 from stepancheg/idris2-time 
Use C idris2_time for all C-based backends
 2021-07-16 09:40:08 +01:00
Edwin Brady
a20aba63ee
Merge pull request #1448 from mattpolzin/case-tree-experiments-merge-upstream 
Case tree heuristics
 2021-07-16 08:47:19 +01:00
Giuseppe Lomurno
07c62e9eef Fixed wrong reflection of records and parameters 2021-07-16 04:28:52 +02:00
Mathew Polzin
89125e96dd merge w/ upstream 2021-07-15 17:21:08 -07:00
Edwin Brady
a880b9884c
Merge pull request #1670 from stepancheg/buffer-names 
Add parameter names to Buffer builtins parameter names
 2021-07-16 00:53:42 +01:00
Edwin Brady
f4cc2f1ea8
Merge pull request #1721 from edwinb/AliasQli-master 
Updated: add doublePow to primitives
 2021-07-15 23:17:53 +01:00
Stiopa Koltsov
c80a502627 Return Bool from IOArray.writeArray 
As suggested in #1677.

Crashing on out-of-bounds might be more practical, but we can
reconsider it later.
 2021-07-15 22:16:22 +01:00
Edwin Brady
4079ae0e25 Merge branch 'master' of https://github.com/AliasQli/Idris2 into AliasQli-master 2021-07-15 21:44:26 +01:00
Edwin Brady
9b0ebcd08b Merge branch 'elab-name-changes' of https://github.com/MarcelineVQ/Idris2 into MarcelineVQ-elab-name-changes 2021-07-15 13:16:47 +01:00
Stiopa Koltsov
291823c752 Remove prim__getErrno from Prelude.IO 
The function is not used, and it is defined incorrectly.
 2021-07-14 03:15:49 +01:00
Stiopa Koltsov
f81c37ea3a Pass Buffer as char* when using C functions in RefC 
To be able to use `C` functions for both Scheme and RefC: it was
not possible for `Buffer` before this PR.

As an example, `writeBufferData` and `readBufferData` functions are
removed: generic C backend implementations are used instead.
 2021-07-13 23:04:36 +01:00
Nick Drozd
9cca3a7d35
Use Not instead of -> Void (#1667) 2021-07-13 15:32:01 +01:00
Johann Rudloff
d5abff4e46
[ fix #1260 ] Use blodwen-stringbytelen instead of C's strlen (#1261) 2021-07-13 11:52:15 +01:00
Stiopa Koltsov
1617d95961 System.Errno.strerror 
* add `strerror` function
* move `getErrno` to `System.Errno`
* use `strerror` in `Show FileError`
* on node there's no access to `strerror`, so `strerror` just converts the number to string
 2021-07-13 10:34:04 +01:00
Stiopa Koltsov
d676ea6ab4 Expose malloc and free from System.FFI 
* Move `malloc`/`free` from `Network.FFI` to `System.FFI`
* Might be useful by other code
 2021-07-13 10:24:26 +01:00
Stiopa Koltsov
ed40b212b2 Make System.Signal async-signal-safe 
It is not safe to call `malloc` or `pthread_mutex_lock` from signal
handler.
 2021-07-12 20:43:26 +01:00
Nick Drozd
a07d42ac91
Delete old Order file, update changelog and contributors (#1685) 2021-07-12 10:53:45 +01:00
Stiopa Koltsov
b4918d51ff Add parameter names to Buffer builtins parameter names 
Also rename `loc` -> `offset`.
 2021-07-11 10:43:12 +01:00
Stefan Höck
599d0635e9
[ refactor ] JS backend overhaul (#1609) 2021-07-10 11:15:21 +01:00
Nick Drozd
61b9a3e4e5
Define and implement Relation interfaces (#1472) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-07-09 09:06:27 +01:00
Stiopa Koltsov
8fd58b3bdd More reliable exception handling in Control.App 
Convert `App.Control.Exception` interface to an alias to `HasErr`.

Probably `Exception` interface need to be deprecated or removed.

Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.

Fix this scenario:

```
throwBoth : Has [Exception String, Exception Int] es => App es ()

throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```

With this commit it works, before this commit it failed with:

```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).

TestException.idr:8:48--8:57
   |
 8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
   |                                                ^^^^^^^^^
```
 2021-07-06 10:43:54 +01:00
CodingCellist
fac0e32f48
[ fix ] Chez channels (#1596) 2021-07-02 13:13:50 +01:00
Alissa Tung
2865a70a6e
[ base ] add List functions (#1550) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-07-01 08:00:12 +01:00
John Mager
dc755e1df5 Pretty instances for IntX 2021-06-30 08:18:37 +01:00
Nick Drozd
9cb20f3653
Clean up some assert_total instances (#1644) 2021-06-29 22:05:40 +01:00
Stefan Höck
39d596f3b9
[ new ] Support reflecting on new intX types (#1642) 2021-06-29 20:58:41 +01:00
Stefan Höck
f5bcc81115
[ new ] Add FromChar and FromDouble interfaces to the prelude (#1641) 2021-06-29 08:37:02 +01:00
Stiopa Koltsov
3d5ad0ca91 Use C idris2_time for all C-based backends 2021-06-28 23:57:58 +01:00
kasiaMarek
6f9b926b1b
module Data.SnocList.Elem (#1478) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-28 20:34:39 +01:00
Stefan Höck
6ed266d306
[ new ] Missing integer type interfaces (#1629) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-28 20:00:10 +01:00
Fabián Heredia Montiel
d5167a0108
[ fix #1581 ] public export Range functions and implementations (#1602) 
Since `[a..b]` uses `takeUntil`/`takeBefore` indirectly those too had to
be changed to `public export` clashing with `Data.Stream` definitions.

A small readability refactor was made with the `compare` function from
`EqOrd`.
 2021-06-28 16:52:23 +01:00
Tim Engler
05f28724ed
[ fix #1579 ] Nat hack for comparison operators (#1580) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-06-28 16:48:08 +01:00
Nick Drozd
63a6b16517 Cut unneeded type specifications 2021-06-28 16:22:27 +01:00
Nick Drozd
f49aa3c001 Simplify a few more lambdas 2021-06-28 15:57:21 +01:00
technic93
0aa968fe56
Add Split and SplitRec views for Vect (#1624) 
Co-authored-by: Denis Buzdalov <public@buzden.ru>
 2021-06-28 15:54:43 +01:00
Kamiλ Shakirov
8e30b296c0
[ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
Stiopa Koltsov
a6555549ee Route System.prim__system through C function 
To be able to eventually refactor/extend `system` function: to be
able to specify a directory, environment variables, specify arguments
as array etc. Ideally it should be something like Rust
[`std::process::Command`](https://doc.rust-lang.org/std/process/struct.Command.html).
 2021-06-28 11:28:14 +01:00
Edwin Brady
d6370380e6 Missing interface methods now cause an error 
This was always the intended behaviour, but until now not implemented!
This caught a couple of issues in contrib and a test.
 2021-06-27 20:03:19 +01:00
Jan de Muijnck-Hughes
939bc8d8ff
Merge pull request #1610 from gallais/fix-golden 
[ fix ] Various Test.Golden fixes
 2021-06-24 20:27:20 +01:00
Guillaume ALLAIS
516b1b18f5 [ fix ] padding shouldn't be affected by ANSI escape codes 2021-06-24 16:38:27 +01:00
Guillaume ALLAIS
c217911573 [ fix ] Only pass --cg to test exec if requested 
Do not pass a codegen choice when the test pool specifies it does
not require a codegen to be specified.
 2021-06-24 16:36:03 +01:00
Edwin Brady
a93def90a9 Merge github.com:idris-lang/Idris2 into prepare-040 2021-06-23 18:16:36 +01:00
Edwin Brady
5689786b26
Merge pull request #1598 from gallais/show-void 
[ fix ] missing Show implementations in libs
 2021-06-23 18:11:40 +01:00
Edwin Brady
7d3e3e0719 Check sizes of buffers and strings in TTCs 
They need to be positive or we can't make the buffer, which causes a
segfault. This happened when loading old TTCs with a different format.
Fixes #1503
 2021-06-23 18:08:27 +01:00
Guillaume ALLAIS
afd55951c2 [ fix ] missing Show (Fin n) in base 2021-06-23 16:46:25 +01:00