idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-04 06:10:15 +03:00
Code Issues Projects Releases Wiki Activity
2,157 Commits 6 Branches 9 Tags 118 MiB
3d5ad0ca91
Commit Graph

686 Commits

Author SHA1 Message Date
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
Edwin Brady
ae73c39609 Merge github.com:idris-lang/Idris2 into prepare-040 2021-06-23 16:17:40 +01:00
Edwin Brady
c1057a19af
Merge pull request #1489 from buzden/some-uninhabiteds 
[ base ] Some lacking implementations for `Uninhabited`
 2021-06-23 16:17:32 +01:00
Edwin Brady
a0cfa28621 Update version numbers 2021-06-23 16:15:21 +01:00
Guillaume ALLAIS
21cca08df1 [ fix ] missing Show Void in prelude 2021-06-23 15:33:12 +01:00
G. Allais
d2986e5fea
[ refactor ] to allow testpools to specify a backend (#1591) 2021-06-21 22:12:17 +01:00
G. Allais
49f8cefeff
[ cleanup ] Test.Golden (#1526) 2021-06-21 17:30:11 +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
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
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
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
Denis Buzdalov
927c358bef [ base ] Some lacking implementations for Uninhabited were added 2021-06-15 15:07:54 +03:00
Nick Drozd
488b4709f4
Use map for some maybes (#1548) 2021-06-14 17:52:43 +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
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
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
Fabián Heredia Montiel
4c99537062 Add color to tests 2021-06-13 10:36:30 -05: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
Edwin Brady
18c7e2c4da Merge github.com:idris-lang/Idris2 into normalise-tweaks 2021-06-10 12:22:02 +01:00
Edwin Brady
7d235272e3 Remove redundant converstion checks in Pi types 
We've already checked argument and scope types, so only need to check
mulitplicities. This saves a lot of repetition when checking lambdas.
 2021-06-10 12:19:41 +01:00
Ruslan Feizerakhmanov
7aee7c9b7c
[ new ] --install-with-src; refactoring around FCs (#1450) 
Why:

* To implement robust cross-project go-to-definition in LSP
  i.e you can jump to definition of any global name coming
  from library dependencies, as well as from the local project files.

What it does:

*  Modify `FC`s to carry `ModuleIdent` for .idr sources,
   file name for .ipkg sources or nothing for interactive runs.

*  Add `--install-with-src` to install the source code alongside
   the ttc binaries. The source is installed into the same directory
   as the corresponding ttc file. Installed sources are made read-only.

*  As we install the sources pinned to the related ttc files we gain
   the versioning of sources for free.
 2021-06-05 12:53:22 +01:00
G. Allais
c5b10f0b52
[ doc ] for the linear pair constructor (#1492) 
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
 2021-06-03 13:04:56 +01:00
madman-bob
98d67499db
RefC Integer Support (#1480) 
* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support
 2021-06-03 10:44:42 +01:00
Denis Buzdalov
29cc1f4248 [ refactor ] Use f <$> ... instead of pure f <*> ... in traverses 2021-06-01 20:28:49 +01:00
Zoe Stafford
24f7c9d5be
Add foldMap to Foldable (#1483) 2021-06-01 15:05:04 +01:00