Commit Graph

3707 Commits

Author SHA1 Message Date
Mathew Polzin
0ea7c599cb allow buildIdris output to be used as a dependency in other buildIdris calls more directly 2024-06-26 15:23:08 -05:00
Michael Messer
5f27842cbc Public export Decidable.Decidable.decision 2024-06-26 08:24:36 +01:00
Mathew Polzin
7d33c0438a
Nix buildIdris improvement: precisely target executable (#3330)
* don't assume all .so files are the exectuable

* don't rebuild support or the compiler if only the buildIdris nix function has changed

* fixes to nix buildIdris function
2024-06-25 19:03:54 -05:00
Robert Wright
3649821625 Add JSON manipulation functions 2024-06-25 10:37:18 -05:00
Sergey Fedorov
a45c587349 idris_signal: fix static_assert 2024-06-24 11:56:23 -05:00
Sergey Fedorov
a38f1acd2f
idris2.ss: support powerpc (#3326)
* idris2.ss: support powerpc

* CHANGELOG_NEXT: support for macOS PowerPC added

* Chez.idr: support macOS PowerPC

* ChezSep.idr: support macOS PowerPC

* chez/support.ss: support macOS PowerPC

* idris2.rkt: support macOS PowerPC

---------

Co-authored-by: Sergey Fedorov <barracuda@macos-powerpc.org>
2024-06-24 11:49:17 -05:00
Denis Buzdalov
ce2790d6f9 [ perf ] Use alternative better GC on chez 2024-06-24 13:34:21 +01:00
Steve Dunham
1a3df3fb62 [ cleanup ] remove unused code left by previous change 2024-06-19 22:21:27 +01:00
Denis Buzdalov
2994e23fd0
[ fix ] Fix search around %defaulthints (#3258)
* [ cleanup ] Move repeating trying-with-unambiguity pattern to a function

* [ fix #2850 ] Search for dependencies for default hints among all hints

* [ fix #2932 ] Always try defaults in dependencies search
2024-06-18 15:39:22 +01:00
André Videla
ddb691bcdc
Merge pull request #3306 from dunhamsteve/implicitParam
[ fix ] implicits are not in scope under an implicit parameter block
2024-06-17 20:03:37 +01:00
Steve Dunham
f9d00ea63e Update comment to cover changes 2024-06-17 10:37:44 -07:00
Guillaume Allais
0c030020de [ re #3314, #34 ] Tighten the location information for implicits
When implicitly binding a variable, use the location of the head
function/constructor that expects it. This way we can differentiate
multiple implicits bound on the same LHS.

Note that this does not resolve the issue 34: there the location
is then further muddled by the fact that where-bound functions
are lifted to the toplevel.
2024-06-17 16:32:24 +01:00
André Videla
d6b8ab980d
Merge pull request #3315 from andrevidela/fix-3302
Emit error when unbound fixity is hidden
2024-06-17 14:11:44 +01:00
G. Allais
3f985bcefa
[ fix #72 ] remove the broken modules (#3319)
* [ fix #72 ] remove the broken modules

People are still hitting the same issueT
There has been no movement towards fixing it
It is IMO unfixable

Let's drop it.

* [ fix #72 ] Remove dependencies of Control.Algebra

Follow-up to the commit by gallais, this removes the contrib libraries
which were using `Control.Algebra`.

* [ fix #72 ] Record changes in CHANGELOG_NEXT

* [ lint ] Move Algebra changes to existing header

---------

Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
2024-06-17 13:45:16 +01:00
André Videla
02e5468551
Merge pull request #3314 from dunhamsteve/issue-3313
[ fix ] auto search returns no solution instead of ambiguous solution #3313
2024-06-17 12:56:20 +01:00
André Videla
0e09b8d575 Show unrelated namespace with matching operator name 2024-06-17 12:39:37 +01:00
Mathew Polzin
e9dfc1c980
List packages improvements (#3318)
* don't show 'Just' before package versions

* unrelated - fix nix develop shell for darwin

* spit out the package path for each package as well as the package name and version

* put the package path on a new line

* add TTC version info to output

* don't name unused variable

* add changelog entry
2024-06-17 11:50:13 +01:00
J. Rinaldi
ecd6d47ea0 Update typedd.rst 2024-06-17 11:47:16 +01:00
André Videla
f67b303cca Emit error when unbound fixity is hidden 2024-06-16 16:10:47 +01:00
Steve Dunham
1807cdcba7 [ fix ] auto search returns no solution instead of ambiguous solution 2024-06-15 15:01:37 -07:00
J. Rinaldi
866354fef1 Update typedd.rst 2024-06-15 12:19:50 +01:00
Steve Dunham
055568be28 [ fix ] case spliting under implicit/auto parameter 2024-06-13 08:40:33 +01:00
J. Rinaldi
f8adee7059 Update typedd.rst 2024-06-12 22:32:18 +01:00
J. Rinaldi
19bc230b0e Update typedd.rst 2024-06-12 21:04:51 +01:00
Steve Dunham
c9f7f308cf [ fix ] implicits are not in scope under an implicit parameter 2024-06-12 12:55:29 -07:00
Steve Dunham
9e84b153bd
Add %foreign_impl pragma for augmenting ffi functions (#3303)
* Add %foreign_impl pragma for augmenting ffi functions

* document how conflicting %foreign_impl are handled
2024-06-11 17:45:09 +01:00
Mathew Polzin
88a5328ec1
Add an option that dumps package details to JSON (#3293)
* Initial stab at package json dump

* expose ipkg json dump as new option

* make dependency output easier to ingest by another tool

* Add a test for ipkg json dump

* cleanup

* maybe just don't collide with existing equally good fixity

* make new operator private

* Add new module to api ipkg file

* Add note to CHANGELOG_NEXT

* correct the docs for the dump-ipkg-json command
2024-06-11 11:32:22 +01:00
Claudio Etterli
0174618724
[ new ] added util functions for SortedMap (#3254)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-11 11:05:48 +01:00
Denis Buzdalov
109033c7b0 [ base ] Move most useful and stable parts of Data.Fin.Extra to base 2024-06-11 10:21:12 +01:00
observant
1e6e125190
Add pipeline operators (#3284)
* Add pipeline operators

* Fix tests

* Change fixity, add tests

* [ fix ] silence actual fixity

---------

Co-authored-by: itmuckel <18561536+itmuckel@users.noreply.github.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2024-06-06 10:59:30 +01:00
troiganto
e0b9a027e7 fix(base): runtime-erase implicit length argument to Vect's dropElem.
This makes it possible to call the function in more situations. It also
brings its signature in line with the overloads on `List`, `List1` and
`SnocList`.

The previous implementation of `Data.Vect.Elem.dropElem` required the
length of the `Vect` to be available at runtime. This was used in order
to recurse in the case that the `Elem` is not `Here`. However, it turns
out that this is not actually necessary. Idris can deduce that the tail
must be non-empty if it contains an `Elem`.
2024-06-05 15:42:48 +01:00
Denis Buzdalov
1522c3a92c
[ fix ] Fix Show of TTImp for functions with with clauses (#2631)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-05 14:02:04 +01:00
Denis Buzdalov
1c588f77ec
[ base ] Add flipped access/update functions for Sorted{Set,Map,DMap} (#3247)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-05 13:59:38 +01:00
troiganto
2c128e216c refactor(base): move implementation of Data.Vect.nubBy to global scope
Closes #3285
2024-06-05 13:53:57 +01:00
G. Allais
bcf8598f99
[ new ] System.Concurrency.(Linear/Session) (#3294)
* [ refactor ] moving Data.OpenUnion to base

* [ new ] System.Concurrency.(Linear/Session)

* [ test ] for the new feature

Fixing other tests impacted by the refactoring

* [ cleanup ] move definitions around, touch up docs

* [ fix ] re-export linear notations for Control.Linear.LIO
2024-06-05 13:53:30 +01:00
Daniel Rainer
7a4c9c89f1 Doc: Use executable command for opening lib docs
The previous command does not work in any shell I am aware of.
The new one directly opens the library documentation in $BROWSER if it
is set and otherwise just echos the path to index.html.
2024-06-05 12:05:01 +01:00
Jorge Gomez
a236bb7a33
fix: typos in "Named Implementations" (#3296)
* fix: typos in "Named Implementations"

* Update docs/source/tutorial/interfaces.rst

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-05 12:03:47 +01:00
MithicSpirit
f83ad9ce98
[ base ] Data.SortedSet.leftMost and .rightMost (#3260)
* [ base ] Data.SortedSet.leftMost and .rightMost

Implement `leftMost` and `rightMost` for `SortedSet` in terms of the
functions with the same name in `Data.SortedMap`.

* contributors

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-05 12:00:57 +01:00
Joel Berkeley
40d4cd898b clarify toMaybeT docstring 2024-06-05 11:59:52 +01:00
Steve Dunham
c0ac024114 [ doc ] Update documentation for with 2024-06-05 11:59:06 +01:00
G. Allais
004f1fd26b
[ new ] Data.SnocList.HasLength from compiler libs (#3299) 2024-06-05 11:51:23 +01:00
Jorge Gomez
0742b3ba97 [ doc ] reference intro info on elab 2024-06-05 07:53:48 +01:00
Jorge Gomez
d7d84868a5 fix: typos in "Expressions" 2024-06-04 13:08:00 +01:00
Denis Buzdalov
a6c5cf5af0 [ fixup #2939 ] Make futures not interfere with optimisations 2024-06-03 15:43:23 +01:00
Aleksei Volkov
10b0cc3240 Updated CHANGELOG_NEXT.md 2024-05-31 10:22:56 +01:00
Aleksei Volkov
167258b975 [ test ] Added regression tests for #2927 2024-05-31 10:22:56 +01:00
Aleksei Volkov
24fcc0b551 [ perf ] Use delay and force to memoize lazy toplevel definitions 2024-05-31 10:22:56 +01:00
Aleksei Volkov
d4f84ab78a [ fix ] Do not lift expressions inside %delay during CSE 2024-05-31 10:22:56 +01:00
Stefan Höck
e73ca067ed
[ performance ] a faster implementation of unpack (#3281)
* [ performance ] a much faster implementation of unpack

* [ fix ] partiality error in Hangman test

* [ test ] add some documentation to the unpack test case

* [ test ] fix expected output of unpack test
2024-05-24 08:06:56 +01:00
Denis Buzdalov
cf68e995c4 [ funext ] Add a proof for funext variants with the other quantities 2024-05-19 15:00:28 +01:00