Commit Graph

41 Commits

Author SHA1 Message Date
Stepan Koltsov
ce44d3b50a
Change semantics of lines and unlines function to match Haskell and other languages (#1585)
* Add trailing newline on non-empty list in unlines

There are several reasons to do that:
* a line in a text file is something which ends with newline,
  and the last line is not special
* `unlines []` should be different from `unlines [""]`
* `unlines (a ++ b) = unlines a ++ unlines b`
* Haskell does it

* Change lines function behaviour
2021-07-17 14:54:23 +01:00
Nick Drozd
63a6b16517 Cut unneeded type specifications 2021-06-28 16:22:27 +01:00
Kamiλ Shakirov
8e30b296c0
[ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
Nick Drozd
0db136d168
Hoist some pures (#1556) 2021-06-16 15:22:52 +01:00
Edwin Brady
d51fe896f7 Trim namespace when writing definitions to TTC
We don't need to write the current namespace every single time! This
won't work as well if there's namespaces in the file, so it needs
refining a bit, but this reduces loading time anyway.
2021-05-18 18:30:06 +01:00
G. Allais
96a2809f62
[ fix #1169 ] primitive types are not NTCon (#1340) 2021-04-28 09:33:27 +01:00
Ruslan Feizerakhmanov
70158b9dd1
REPL commands: load-package & fuzzy-search (#1318)
REPL commands: load-package & fuzzy-search
Move REPL-related code over to its own namespace
2021-04-25 09:13:55 +01:00
Guillaume ALLAIS
96cc7fd273 [ new ] depthFirst, findFile 2021-04-19 10:58:40 +01:00
G. Allais
5946442dc2
[ new ] idris2 --init (#1299) 2021-04-15 14:08:50 +01:00
Andy Lok
da92f9d676
Cleanup List1 (#1091) 2021-03-17 14:07:52 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base (#1033) 2021-03-04 20:59:56 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095) 2021-02-24 11:07:16 +00:00
Denis Buzdalov
b355b12cdb Some cleanup was done. Changed code is mosly equivalent to the former.
A lot of useless matches of implicit arguments were removed.
2021-02-16 19:05:33 +00:00
Wen Kokke
bd683938bf
Overhaul of concurrency primitives (#968)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-02-05 16:16:20 +00:00
Stefan Hoeck
0906ac30b9
added System.Console.GetOpt to contrib (#974) 2021-01-21 17:59:06 +00:00
Stiopa Koltsov
b76c9d91e0 Remove trailing whitespaces and add trailing newlines 2021-01-16 10:00:03 +00:00
Andy Lok
4f8bd22b35 Use present tense in doc for Path 2021-01-14 05:26:42 +08:00
Andy Lok
f1d6d4d6f4 Use dot syntax to avoid path argument 2021-01-14 05:05:59 +08:00
Andy Lok
9f72a514f1 Rename startWith to isBaseOf 2020-12-07 15:26:00 +08:00
Andy Lok
5578761bdb Improve splitPath 2020-12-07 05:19:53 +08:00
Andy Lok
d3a74e0199 Update document 2020-12-07 04:27:54 +08:00
Andy Lok
f5e0853264 Refactor Utils.Path 2020-12-07 04:16:28 +08:00
Andy Lok
8eea90527a Refactor System.Path 2020-12-07 04:10:15 +08:00
Fabián Heredia Montiel
57a8ef4609
Implement Futures as a Parallelism Primitive (#753)
Co-authored-by: Christian Rasmussen <christian.rasmussen@me.com>
2020-12-04 10:58:26 +00:00
russoul
3a9b1ac656 Add supporting code 2020-08-25 14:30:57 +03:00
russoul
594105d5ac Eliminate schemeCall from the library 2020-08-24 19:38:29 +03:00
Kamil Shakirov
8544e80076 Use the same naming convention for foreign primitives 2020-08-19 14:05:28 +01:00
Edwin Brady
dbdf7dab3d Back to HasIO, remove MonadIO
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:

- it's easier for backend authors if the type of IO operations is
  slightly less restrictive. For example, if it's in HasIO, that limits
  alternative implementations, which might be awkward for some
  alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
  be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
  instance (I have personally never encountered one - if they turns out
  to exist, again, we can revisit!)
2020-06-21 19:21:22 +01:00
Edwin Brady
1b15463746 Update libraries and docs with HasIO/MonadIO 2020-06-21 15:25:40 +01:00
Edwin Brady
3f914889b8 Add visibility rules on types
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
2020-05-30 17:03:15 +01:00
andylokandy
f007c7816e Sync Utils.Path with System.Path 2020-05-30 21:51:12 +08:00
Edwin Brady
e067355c58 Allow parsing multiple separators in Path
Might help with #194
2020-05-30 11:19:28 +01:00
Niklas Larsson
696db7f58f
Merge pull request #169 from andylokandy/pathcom
Use Path in the compiler
2020-05-27 21:23:29 +02:00
Edwin Brady
c88bf7af8d Fix import loading
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)

This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
  Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
  things were being imported that shouldn't have been. The new way is
  correct!

An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
2020-05-27 15:49:03 +01:00
andylokandy
712a4df140 Gather the straw isWindowss 2020-05-26 17:59:14 +08:00
Niklas Larsson
77df65012c Fix Path ambiguity 2020-05-23 11:08:25 +02:00
Kamil Shakirov
806c993d99 Move System.Clock from 'contrib' to 'base' 2020-05-21 17:00:09 +06:00
Marek L
1a998d8944 Fix typo seperate -> separate in System/Path.idr
https://www.grammarly.com/blog/separate-seperate/
2020-05-21 09:28:11 +01:00
andylokandy
8de668f1a4 Add folds without default value to List 2020-05-21 02:09:14 +08:00
andylokandy
0d82b5d7da Add System.Path 2020-05-20 22:51:01 +08:00
Edwin Brady
dec7dff622 Add libraries 2020-05-18 14:00:08 +01:00