Commit Graph

702 Commits

Author SHA1 Message Date
Denis Buzdalov
715a304137 [ elab, minor ] Implement Functor for PiInfo 2024-06-27 15:51:32 +01:00
Michael Messer
5f27842cbc Public export Decidable.Decidable.decision 2024-06-26 08:24:36 +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
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
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
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
G. Allais
004f1fd26b
[ new ] Data.SnocList.HasLength from compiler libs (#3299) 2024-06-05 11:51:23 +01:00
Denis Buzdalov
cf68e995c4 [ funext ] Add a proof for funext variants with the other quantities 2024-05-19 15:00:28 +01:00
stefan-hoeck
e1c5c2fd8e [ fix ] issue 3266 2024-04-22 15:44:35 +02:00
Ellis Kesterton
2823281af6
Add partiality/delay monad (#3240) 2024-04-04 11:53:11 +01:00
André Videla
75032a7164
Emit warning for fixities with no export modifiers (#3234)
* Emit warning for fixities with no export modifiers

This is to help update all the existing code to program with explicit
fixity export directives in preparation for the behavioral change where
they will become private by default.
2024-04-03 15:41:57 +01:00
Mathew Polzin
7ce4c45e82
Complete the relocation of contrib HVect into base as All (#3191)
* complete the relocation of contrib HVect into base as All

* Frex needs these public exported and that feels reasonable enough to me

* Add CHANGELOG_NEXT entries
2024-03-19 08:22:32 -05:00
Jacob Walters
18b165bede [ elab ] Let elab scripts access visibility modifiers 2024-03-15 22:41:29 +00:00
Mathew Polzin
7219486aec
Fix ambiguity error with Uninhabited interface implementations. (#3228) 2024-03-15 17:21:05 -05:00
rvs314
1143718098
Generalize succNotLTEpred (#3225)
* Don't require a runtime value of `x` for `succNotLTEpred`

* Add `succNotLTEpred` as an instance of `Uninhabited`

* Add contribution to changelog

* Update golden value for test `basic044`
2024-03-07 08:38:28 -06:00
Denis Buzdalov
8144980ae5 [ elab ] Support easy collection of information during TTImp traverse 2024-02-23 11:32:22 +01:00
Denis Buzdalov
9ab96dacd4 [ elab ] Treat map and <*> with no bind in elab scripts runner 2024-01-17 17:45:19 +03:00
Mathew Polzin
073fbef3d1
Remove use of deprecated getByte function (#3190)
* Add CHANGELOG_NEXT entry
2024-01-14 11:26:51 -06:00
Joel Berkeley
ee18555869
Add (++) for List variation of All (#3179)
* Add `(++)` for `All` for `List`

* changelog

* contributors

* review changes

* update comment

* update comment

* match TODO style

* disambiguate the right one

* further comment changes
2024-01-01 21:03:13 -06:00
Denis Buzdalov
3fe95d469a [ interpolate ] Implement Interpolation for primitive numeric types 2023-12-29 11:17:31 -06:00
Denis Buzdalov
db4f65bd8d [ refactor ] Move lazy lists from contrib to base 2023-12-29 09:22:03 -06:00
Denis Buzdalov
82bb12cf72 [ cleanup ] Post v0.7.0 cleanup 2023-12-25 13:49:26 +00:00
Thomas E. Hansen
ea180d0721 [ rc ] Prepare for 0.7.0
A lot more sensible all around  : )
2023-12-22 14:44:30 +01:00
Thomas E. Hansen
a3b078cb0d [ rc ] For v0.6.9 - to see if the process was right
Good luck everybody...

v0.6.9 - Nice!  ^^
2023-12-22 14:44:30 +01:00
Denis Buzdalov
da916b68d4 [ fix ] Correctly manage the empty file case while reading a file 2023-12-21 13:30:30 -06:00
Denis Buzdalov
b495fe83f0 [ fix ] Support waiting for popen2-created processes
This fixes problem of creation the garbage of zombie processes on POSIX
systems. This also makes behaviour of `popen2` identical in Windows,
namely, all resources are freed only when waiting, giving at the same
time an ability to observe the exit code afterwards.
2023-12-19 23:03:31 +03:00
Denis Buzdalov
eddcbcdc75 [ base ] Add modifyRef into the Ref interface 2023-12-08 18:54:57 +00:00
Denis Buzdalov
8557b5b810 [ typo ] Fix a silly typo 2023-12-08 18:54:57 +00:00
Andor Penzes
82e4fd9da7
Add foldrImplGoLemma to Data.Vect (#2835)
Co-authored-by: CodingCellist <teh6@st-andrews.ac.uk>
2023-11-30 10:07:41 +00:00
0xd34df00d
6dd25cd9ec [ base ] Add mapPropertyRelevant, tabulate and (++) for Vect's All 2023-11-30 09:53:05 +00:00
G. Allais
b08efbea40
[ refactor ] split Core.TT (#3151) 2023-11-29 20:24:01 +00:00
Denis Buzdalov
2c328a51c0 [ elab ] Support more applicative traversals of TTImp 2023-11-09 22:05:36 +00:00
CodingCellist
d80bc1537d
[ base ] Add bindings for ieee Double number consts (#3116) 2023-11-09 14:01:40 +00:00
Denis Buzdalov
64ad807f83 [ deriving ] Try to reduce a type before searching it's showable 2023-10-30 10:07:39 +00:00
G. Allais
bee59d5fde
[ fix ] missing modules in .ipkg files (#3124)
Additionally, we now have bash options to make sure we will fail hard were
this situation to arise once again.
2023-10-27 20:37:00 +01:00
Denis Buzdalov
5f29b0b9c5 [ elab ] Add an ability to inspect in which function we currently are 2023-10-26 15:42:26 +01:00
Denis Buzdalov
50a579fa18 [ elab ] Implement an operation of returning referred defs of a def 2023-10-26 15:42:26 +01:00
Adowrath
ea093ffaed
[ warning ] for incompatible visibilities on forward decls and definitions. (#3063) 2023-10-25 11:24:43 +01:00
Denis Buzdalov
305604d243
[ base ] Implement a bunch of standard interfaces for Data.These (#3117)
* [ base ] Implement a bunch of standard interfaces for `Data.These`

* [ base ] Add couple of eliminators with default values for `These`
2023-10-25 11:15:28 +01:00
Denis Buzdalov
6c35157087 [ ux ] Make isType fail with positioned errors 2023-10-17 18:05:54 +01:00
Denis Buzdalov
f64047b9ac [ safe ] Set deriving escape hatches to be marked as %unsafe 2023-10-17 18:05:54 +01:00
Denis Buzdalov
2358a74a29 [ base ] Implement Zippable for several standard types + small cleanup 2023-10-16 22:41:55 +01:00
0xd34df00d
7c8076c149 [ base ] Relevant and irrelevant traversals for Data.Vect.Quantifiers.All 2023-10-16 09:49:22 +01:00
0xd34df00d
f2a95071a1
[ base ] Add Data.Vect.Quantifiers.All.remember, the inverse to forget (#3096)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-10-13 15:26:24 +01:00
Stefan Höck
7fbbb030df
[ new ] add Data.List.grouped function (#3089) 2023-10-13 13:48:15 +01:00
Denis Buzdalov
f7d4b7f4ed [ base ] Add a bridge between MonadState and Ref 2023-10-13 13:47:31 +01:00