Commit Graph

1094 Commits

Author SHA1 Message Date
Denis Buzdalov
bbe96929f1 [ minor, base ] Relax requirement of the These.bifold 2023-01-26 22:15:15 +00:00
Denis Buzdalov
f4b44ba109 [ prelude ] Make some higher-kinded functions be tc-inlined 2023-01-25 16:51:11 +00:00
Marek L
7ec96cea7f [ doc ] Remove typo from Prelude.plus doc string and
reformat doc string for `Prelude.minus`
2023-01-24 23:35:03 +00:00
Mathew Polzin
4bedaac811
[ fix ] make color output toggling simpler and also more robust. (#2848)
* make color output toggling simpler and also more robust

* don't unintentionally assert that tests are run in an environment where colors are turned on.

* Update src/Idris/Env.idr
2023-01-22 13:35:57 -06:00
G. Allais
ea4a4c0f85
[ base ] fix the definition of die (#2854) 2023-01-19 11:09:28 +00:00
Mathew Polzin
24ac56de88
Moving Data.List.HasLength into base (#2844) 2023-01-16 00:07:21 -06:00
Denis Buzdalov
936b7270ae [ prelude ] Add lacking implementation of Traversable for Pair 2023-01-09 15:56:21 +00:00
Mathew Polzin
4005b40a95
[new] Vect.Quantifiers.All QoL (#2843)
* Add Show for Vect.All

* Add an alias for HVect to Data.Vect.Quantifiers.All

* Add a few utilities for Vect.Quantifiers.All to make it more at home in listy uses.

* Add CHANGELOG entries.
2023-01-09 00:57:00 -06:00
Stefan Höck
8db12f5a49
[ performance ] improve some Char functions (#2839) 2023-01-06 09:08:38 +00:00
Zoe Stafford
ae2d4efc17 add javascript support to System.Clock
This may behave incorrectly when used with web workers
2022-12-22 11:47:44 +00:00
Zoe Stafford
18ffb852de export {to,from}Nano in System.Clock
also rename some arguments and add docs
2022-12-21 15:49:32 +00:00
Denis Buzdalov
f4ebcadfad [ base ] Add forgetting conversions of Vect.Quantifiers 2022-12-20 16:36:27 +00:00
G. Allais
2f55a3ef8a
[ fix ] elaboration of records' telescopes of parameters (#2816) 2022-12-15 17:55:50 +00:00
Denis Buzdalov
ff6afb0c59 [ minor ] Make NotBothZero parameter of standard gcd to be erased 2022-12-05 15:10:16 +00:00
Denis Buzdalov
8d7b993cca [ cleanup ] Use several library functions instead of their code 2022-12-05 15:10:16 +00:00
Denis Buzdalov
33fe3f44db [ cleanup ] Clean up existing code in the Arrow module 2022-12-05 15:10:16 +00:00
Guillaume Allais
99eda4dd2b [ papers ] fill last hole in lambda pi formalisation 2022-12-05 15:02:04 +00:00
G. Allais
85bb822f3b
[ perf ] manually eta-expand unsaturated io_bind calls (#2785) 2022-12-01 15:31:00 +00:00
G. Allais
f96c5ca596
[ papers ] LambdaPi (#2780) 2022-12-01 13:48:48 +00:00
0xd34df00d
c6a8c9e7a7 [ base ] Move the worker outside of the Vect's reverse definition 2022-11-21 10:52:47 +00:00
Tim Engler
bff18428b4 Added seqL to Control.App and updated docs to fix #2761
Also updated test real002 to use the actual Control.App from
libs/base/Control/App.idr. Before it was using a different version that
existed within its test directory, tests/idris2/real002/Control/App.idr
2022-11-21 10:39:43 +00:00
Hattori, Hiroki
5c9f8e36a1
[ RefC ] Add 16 and 32 bit access to base/Data.Buffer . (#2609)
* Fix symbom mangling

* Revert "Fix symbom mangling"

This reverts commit 6481e80155.

* Fix typo

* [RefC] Add missed prims of setBuffer* .

* [ fix ] formatting

* [ re #2609 ] Use 'UInt' instead of 'Word'

More descriptive/to the point / Less assumed knowledge.

There are no *LE suffixes for UInt8, since endianness is to do with
multiple bytes and UInt8 is a single one.

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
2022-11-15 12:15:06 +01:00
CodingCellist
70ef197cf6
[ base ] Deprecate setByte in favour of setBits8 (#2764)
* [ base ] Deprecate setByte in favour of setBits8
           Deprecate getByte; fix Core.Binary.Prims

Along with `setByte`, the `getByte` function should similarly be
deprecated since it also assumes the value will have the given size,
rather than guaranteeing it in the type.

CI highlighted some required changes in `Core.Binary.Prims` thanks to
`-Werror`. The fix was to add some `cast` calls where the old `getByte`
and `setByte` used to be.

The RefC buffer test will need updating once we remove the functions
completely. Added a note for future peeps.
2022-11-15 10:42:07 +01:00
Robert Wright
b2c42280bb Erase Fin fromInteger upper bound 2022-11-11 15:34:58 +00:00
Guillaume Allais
8556c81014 [ new ] typed ABT 2022-11-04 16:20:46 +00:00
G. Allais
fd46e31da3
[ new ] typed Krivine (#2749) 2022-11-04 10:05:31 +00:00
stefan-hoeck
6f5b19c389 [ cleanup ] bifoldMap already in Prelude 2022-11-03 14:11:15 +00:00
G. Allais
ad817538e0
[ new ] typed SECD (#2743) 2022-11-02 12:58:13 +00:00
G. Allais
4cd38a8c5d
[ new ] deriving Show (#2741) 2022-11-02 11:57:07 +00:00
G. Allais
ee8113bb9d
[ papers ] A Completely Unique Account of Enumeration (#2659) 2022-11-01 16:31:57 +00:00
Stefan Höck
85ddafbac5
[ fix ] bump version of linear and papers packages (#2735) 2022-10-28 08:55:35 +01:00
Edwin Brady
e125c9014f
Prepare release 0.6.0 (#2733)
* Prepare release 0.6.0

* Fix bootstrap chez

* Correct version in bootstrap chez
2022-10-27 16:32:16 +01:00
Stefan Höck
57c589ca80
[ performance ] More stack safety in the Prelude (#2704) 2022-10-26 09:54:53 +01:00
Aleksei Volkov
c906720ee3
[ base ] Change Reader to fix search for MonadReader instance (#2729) 2022-10-22 19:13:52 +01:00
G. Allais
475d13bb11
[ fix ] parsing of test lib's options (#2725)
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2022-10-21 21:01:54 +01:00
CodingCellist
47c2de3148
[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)
A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.

Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.

This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.

* [ repl ] Use unlines for detailed help (see #2087)

  Ideally, the lines affected should be multiline strings. But for some
  arcane reason, newlines in those get swallowed in Nix and Windows
  **CI** only Ô.o
  This was already documented in issue #2087.

* [ new ] --except for golden testing lib

  To allow CI to pass despite #2087

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-21 14:35:33 +02:00
QDelta
e0a19aa01e
[ fix #2719 ] --only behavior in Test.Golden (#2720)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-18 12:36:09 +01:00
Denis Buzdalov
eb4cc0054b [ golden ] Make options to store more flexible tests filter 2022-10-14 15:03:05 +01:00
Denis Buzdalov
2744a3a5a2
[ golden ] Truncate long test names when printing the results (#2553) 2022-10-06 19:18:34 +01:00
Thomas E. Hansen
bdbc0c72bf Make the linter happy 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
cfe18b3d01 [ papers ] A bit of tidying up and clarification 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
d25db9e353 [ papers ] Add implementation of Dekker's algorithm
This completes the implementation of the examples in the paper
"Applications of Applicative Proof Search" (Liam O'Connor, 2016).
Unfortunately, the final example is an example of something that _can_
be expressed, but _cannot_ be model-checked by the approach in the
paper.

(Side note on `petersonsCorrect`: The paper mentions that it checks in
~3 minutes on a 2013 MacBook Pro. Assuming they mean "type-checks", this
is roughly consistent with our observations of just short of 2 minutes.
I doubt that they evaluated it, since an attempt at doing this on a
reasonably modern server (Intel Xeon Gold 5220R, 502 GB of RAM) was
killed after just over 3 hours, producing the following resource log:

  Command exited with non-zero status 255
  Time: 11320.46s user, 35.12s system, 3h09m46s elapsed, 99%CPU
  Memory: 57644016 Kbytes RAM

)
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
260d9ecb58 [ papers ] Comment out petersonsCorrect for performance reasons
On average across 10 runs on an Intel Core i7-8750H with 15.2GB of
available system memory (16GB installed in system), type-checking
`libs/papers/Search/GCL.idr` WITH `petersonsCorrect` takes:

  * 1 minute  48.7 seconds, consuming 3.92GB of RAM

By contrast, commenting `petersonsCorrect` out results in type-checking
taking on average (same #runs, same config):

  * 0 minutes  1.2 seconds, consuming 0.25GB of RAM

And good luck trying to evaluate the thing!
(This might be a good performance test at some point, but uh, we're not
there yet...)
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
c5b114209e [ papers ] Tidy the Peterson's Prop type
Inspired by `Search/Properties.Pythagoras.formula`, having the CSP as
its own type allows for some better docs+understanding than `Prop ? ?`.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
d5c9253e7e [ papers ] Fix impl.n s.t. model-checking Peterson's works
Thanks to the debug info supplied by #2673, I was able to spot which
functions were blocking and `public import` the relevant files in
`papers/Search/Properties.idr`.

As a result the GCL file now type-checks, albeit extremely slowly!
I stopped an evaluation of `petersonsCorrect` at the REPL after 15
minutes and ~14GB of RAM consumed.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
36554eb56f [ papers ] Make ops total, implement termination mc
* Currying the `ops` function makes the totality checker spot that it
  _is_ actually total.
* Instance arguments are heavily abused in the paper, along with
  implicit `open` magic, but Idris allows no such ~~luxury~~
  obfuscation, so we have to pass things explicitly.
* `decSo` is not `public export`ed, so we have to define `IsTT` by
  pattern-matching (which is fine).

Currently, it gets stuck on checking `petersonsCorrect` for some,
currently unknown, reason. (And the log output is loooooong O.O)

Once again, this would not have been possible without gallais insigths.
Many thanks!

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
8c76118f2f [ papers ] Finish Search.CTL
* Switch to `Inf` to actually use codata/corecursion.
* Add `%hint`s to mark the interface implementations as such, despite
  use of a record for `DepthInv` (this is necessary for other stuff).
* Pass in `Oh` to `reaches10.evidence` in order for things to work.

With huge thanks to gallais for helping me put the final things in
place!

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
0d72964f21 [ papers ] Missed some public exports 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
eb4749d381 [ papers ] Figure out types, start termination check
Termination checking needs figuring out. There is some funky stuff going
on with the half-deciders and their constructors. Other than that, I
**think** it's nearly done. God knows how much RAM it'll take though...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
6421973282 [ papers ] Add mutex and starv-free properties 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
5742afe3a5 [ papers ] Set the stage for mc-ing Peterson's alg 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
8ca48e0033 [ papers ] Implement reaches10 proof
Seems to be very slow though...
And Idris is unable to find the depth-inv instance for `r10Proof`.
Could be that auto-search is not as strong as Agda's? Or more likely,
I've set things up slightly wrong...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
5f48fbe857 [ papers ] Add derived GCL control structures 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
92ed8607e3 [ papers ] Start implementing GCL
I am upset about the amount of computation done in that view...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
b3a8d344e4 [ papers ] Implement proof-search for EF, AF, EG, AG
This also caught an implementation error in the Global formula
definitions:
AG f = A[ f U (f AND' Completed) ]
and **not**
AG f = A[ (f U f) AND' Completed ]
(both of which are valid parsings of the original
 AG f = A[ f u f AND' Completed]
 )
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
f96b25a3d7 [ papers ] Keep AF, EF, AG, EG naming consistent 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
81df879c77 [ papers ] Define Finally operators 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
58b6ccdaf3 [ papers ] Change to LazyList for Computation Tree
This makes more sense in terms of `EU` being efficient and only
evaluating as much as it needs to. However, I'm not sure `model.follow`
is implemented correctly (Agda delays the call to `model.followAll`,
which I'm unsure if we can do (and if so, how to do it) in Idris)...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
68f8e69ea2 [ papers ] Impl.t proof-search for AU and EU
This reveals an unfortunate problem/misunderstanding: For `ExistsUntil`
to make sense, in terms of evaluation speedups, the list needs to be
lazy. Which is _not_ what `Lazy (List a)` does /!\
I need to switch to LazyList...
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
40780c8f85 [ papers ] Figure out isCompleted by trial and error
And here's a good case against allowing custom unicode syntax:
〈$〉 is `<$>`, i.e. the infix notation for `map`. That's fine; If you
happen to know it!
ESPECIALLY, if your paper defines 〈_〉 as custom notation for a guarded
expression! Then there is **no way** to tell that the expression 〈$〉
is not a guarded expression over `$`, but is instead the alias for
`map`!! You just have to magically know this beforehand!

We also need an explicit `Lazy` annotation for Idris to be happy with
the implicit `ms` in the `IsCompleted` constructor.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
67218e3eac [ papers ] Move LTE' outside parameters block 2022-10-05 14:30:08 +02:00
Thomas E. Hansen
3e0d5acfa4 [ papers ] Map depth-invariant prfs for AU and EU
The proofs of depth-invariance for Always Until and Exists Until require
mapping the proofs over the Formulae's internal `All` and `Any`
respectively. Idris provides some functions for this, but they erase the
list and so don't quite work. Instead we need to implement our own,
which don't erase the list.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
40e1a53ab2 [ papers ] Cleaned things up a bit; utterly confused
Don't you love when papers introduce syntax and functions which you've
never seen before and don't seem to match the types of the existing
stuff?

P.S. YEET! (aka. that's probably enough for today ^^)
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
db30dd8d4a [ papers ] Fix things by adding a parameter block
The original Agda code declares the module with L and Sigma (Lbls and
Sts) with type Set. This is apparently close to a parameter block, which
solves the unification error I was having with `now`! Huge thanks to
gallais for showing me that!
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
0c72f83fe8 [ papers ] Start implem.g the model-checking part of Liam's paper
I should have put this under version-control WAAAAAY sooner than this!
Oh well, better late than never...

There are some fun problems to solve in terms of type-mismatch and
erasure, but that's for another day.
2022-10-05 14:30:08 +02:00
Thomas E. Hansen
a90fe03ff7 Add DOI to Liam's search paper stuff 2022-10-05 14:30:08 +02:00
G. Allais
1f3809c49a
[ re #2675 ] Do not build libs/{contribs,papers} during bootstrap (#2677)
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
2022-10-04 13:37:45 +01:00
Zoe Stafford
138452273c
Merge pull request #2701 from stefan-hoeck/snocfold
[ performance ] efficient foldr and foldMap for SnocList
2022-10-04 12:52:39 +01:00
stefan-hoeck
0e956249cc [ performance ] efficient foldr and foldMap for SnocList 2022-10-04 12:19:32 +02:00
Sam Phillips
ba34b64c68 Remove note about differing behavior 2022-10-04 10:24:27 +02:00
0xd34df00d
c2dd824c58 [ base ] Implement Uninhabited for impossible Pointwise equalities 2022-10-02 21:41:26 +01:00
Denis Buzdalov
f58a96e420 [ papers ] Move a postulate to a required parameter 2022-10-01 15:11:26 +01:00
hilary888
9eaff9f728 Fix typo in documentation string 2022-09-30 22:35:36 +01:00
Stefan Höck
7eebeff905
[ fix ] natToFinLt is O(n) (#2689) 2022-09-29 14:36:32 +01:00
Denis Buzdalov
1402194f14 [ golden ] Split runner to be able to run with custom options 2022-09-27 22:05:12 +01:00
André Videla
162d9e942b
Merge pull request #2686 from dunhamsteve/lexer-issue
[ fix ] Lexer reports incorrect column numbers
2022-09-27 16:00:27 +01:00
stefan-hoeck
de216d3ced [ fix ] drop first command-line arg on node 2022-09-27 08:19:14 +02:00
G. Allais
81ea363ae8
[ base ] deriving Traversable (#2678) 2022-09-24 12:43:49 +01:00
Guillaume Allais
5631608782 [ base ] deriving Foldable 2022-09-24 10:20:25 +01:00
Denis Buzdalov
ac9e03d7e3 [ base ] Add a variant of System.run allowing processing on the fly 2022-09-22 14:01:03 +01:00
wwww
38db7c3d22
[ fix ] showTime pads nanoseconds properly (#2650) 2022-09-22 12:18:26 +01:00
Stefan Höck
08f24e79fd
[ performance ] constant folding for all integral expressions (#2662) 2022-09-21 10:05:02 +01:00
Joel Berkeley
c0153e72cd
[ base ] implement decEq for SnocList (#2630)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-09-20 15:46:15 +01:00
G. Allais
d1ae9d9fd5
[ papers ] Computing with Generic Trees (#2661) 2022-09-16 11:40:09 +01:00
G. Allais
55926f30c5
[ fix #2655 ] Add support for DataOpts in records (#2658) 2022-09-14 14:57:04 +01:00
Yupanqui
93b0f9c7b8 Fix for lexer colums 2022-09-05 13:47:41 -07:00
0xd34df00d
b3c80e0765 [ base ] Add finToNatEqualityAsPointwise, an inverse of finToNatQuotient 2022-09-05 12:45:28 +01:00
Steve Dunham
351b5ba720 [ parser ] Fix issue where Alt drops incoming commit tag 2022-09-05 12:44:02 +01:00
Adowrath
1914606d40 Fix connect in linear module and add bytes-specific functions 2022-09-01 12:23:29 +01:00
Denis Buzdalov
5266a2bc22 [ base ] Implement MonadError () for MaybeT 2022-09-01 10:48:15 +01:00
Guillaume Allais
6891490ed2 [ fix ] support for implicits in Deriving.Functor
A lot of refactoring to bring these. That's hopefully the last
feature that was needed...
2022-08-29 18:35:24 +01:00
Zoe Stafford
86c060ef13
Reimplement %nomangle in terms of %export (#2604)
* Reimplement %nomangle in terms of %export
Also deprecate %nomangle

* [ lint ] fix linter errors
2022-08-15 13:26:06 +01:00
Guillaume Allais
4672305fc3 [ fix ] more filtering of invalid datatypes 2022-08-13 11:29:19 +01:00
Steve Dunham
e29e2289e7
[ fix ] Fixes memory leaks in currentDir, fGetLine, and fGetChars (#2606) 2022-08-10 21:23:53 +01:00
Nil Geisweiller
719b5ad17f
[ cleanup ] Remove extraneous show and simplify printLn (#2618) 2022-08-10 21:22:58 +01:00
G. Allais
0cbbf97b79
[ new ] extend Deriving.Functor to (non-strictly) positive functors (#2591) 2022-07-18 14:10:46 +01:00
Mathew Polzin
4a348c1f95 Public export remaining function to allow for proofs involving parsing numbers. 2022-07-18 14:10:05 +01:00
ProofOfKeags
68a144bf18
Support System.Signal for node backend (#2556)
* first pass at signal support for node backend

* change signal values to int's

* implements defaultSignal

* return -1 as expected by calling API if any error is raised by nodejs runtime

* finishes signal support for nodejs

* extract repetitive foreign import identifiers

* fix comments
2022-07-10 10:18:58 +01:00
stefan-hoeck
ea6f9975cf [ cleanup ] add proper depends field to network.ipkg 2022-07-07 17:24:54 +01:00
Guillaume Allais
8b20da7e39 [ cleanup ] remove TT from base
As discussed with edwin, let's get rid of the external TT type.
There is no way to get your hands on a TT value anyway so this
should not change anything.
2022-07-07 16:42:19 +01:00