Commit Graph

185 Commits

Author SHA1 Message Date
Rohit Grover
edb063eb50 Add System.Clock to fetch current time for various clock types. 2020-05-09 17:21:23 +12:00
Edwin Brady
30b609d55f readFile needs a newline
This isn't strictly right yet (there should be no newline on the last
lie if there was no newline in the input file) but it puts the behaviour
back to what it was before fGetLine was changed to discard it.

This needs revisiting...
2020-05-04 21:05:51 +01:00
Edwin Brady
085f6806da
Merge pull request #322 from rbarreiro/copy_json_from_idris_dev
added json
2020-04-27 15:29:44 +01:00
Edwin Brady
d0a9f9e9a6 Move takeBefore/takeUntil to Data.Stream
They're not total, so shouldn't be exported from the Prelude - they are
kept there for range syntax though.
2020-04-27 15:25:25 +01:00
Edwin Brady
61fae5c040
Merge pull request #310 from Kaiepi/bsd-builds
Fix builds on *BSD
2020-04-27 15:21:37 +01:00
Edwin Brady
cbd88c9f2e
Merge pull request #316 from abdelq/master
Adding corresponding toFileError for FileExists
2020-04-27 15:17:34 +01:00
Edwin Brady
c95c4c6c0c
Merge branch 'master' into prelude-inline-doc 2020-04-27 13:38:29 +01:00
Edwin Brady
ff86f6f834 Implement occurs check properly (finally!)
Instead of the previous unreliable hack, actually look for occurrences
of the solved metavariable. Block if there are any, and fail if there
are any under a constructor. I had expected this to hurt performance
quite a bit, but it seems it doesn't.
This was prompted by #304, which is now partly fixed, but there's still
a refinement to unification needed to fix it fully (and at least it
doesn't segfault due to the cycle now!)
2020-04-27 12:17:45 +01:00
Rui Barreiro
bb6aaad373 added json 2020-04-25 19:45:29 +01:00
Abdelhakim Qbaich
55bc68a10e Add missing FileExists in toFileError 2020-04-23 23:16:14 -04:00
Edwin Brady
3d8d07621d Some inlining changes
Flags can now be set on implementations too, where the flags get passed
to each of the methods in the implementation. We might want something a
bit more fine grained than this later. Also some small changes to the
way inlining lets is done in the compiler.
2020-04-23 20:01:20 +01:00
Ben Davies
93871c5fb9 Fix builds on *BSD
This makes it so gmake gets used instead of make on *BSD, refactors how
platforms are handled in general.
2020-04-22 11:09:05 -03:00
Kamil Shakirov
5b58bf2cc1 Add missing export 2020-04-22 11:21:12 +06:00
Kamiλ Shakirov
0c7b553e23
Oops 2020-04-22 08:48:38 +06:00
Kamil Shakirov
35994b81e9 Port prelude's inline API documentation from Idris 1 2020-04-22 01:40:40 +06:00
Edwin Brady
5ea11cf0f5
Merge pull request #282 from abailly/network-binary
provide building blocks for binary network I/O
2020-04-21 10:45:52 +01:00
Edwin Brady
1734841275 Add a lambda lifter
It's not actually used as part of any compilation pipeline yet, and I've
only tested it by eyeballing the output, but it'll be useful soon, and
it's good for it to be available to any new back ends that might need
it. It will need some optimisation.
2020-04-19 22:57:10 +01:00
Arnaud Bailly
2b0cc2a592 provide building blocks for binary network I/O 2020-04-14 21:15:32 +02:00
Edwin Brady
69a7640a6e Allow flagging types as externally defined
e.g. in a C file. This means we don't accidentally treat things as
empty, since previously we just defined these as empty types, but that
broke coverage checking. Fixes #240
2020-04-10 11:45:52 +01:00
Edwin Brady
211fc359ca Erase %World for the purpose of newtypes
We never inspect it, so it carries no information - it just needs to be
there as a token to make sure that IO operations run at the right time.
So, IORes can be a newtype now and therefore optimised away.
2020-04-09 00:20:37 +01:00
Guillaume Allais
c5903c45e1 [ cosmetic ] various whitespace issues 2020-04-02 17:31:15 +01:00
Edwin Brady
7c0581a10a
Merge pull request #245 from ziman/stable-sort
Make `List.sortBy` stable
2020-03-31 18:15:27 +01:00
Edwin Brady
04c63b593f
Merge pull request #243 from deviant-forks/intercalate-list
Add `intercalate` for `Data.List`
2020-03-31 18:14:29 +01:00
Edwin Brady
7ff1e6275f Allow setting logging mid term
Sometimes this makes debugging easier since the logging is more
localised.
2020-03-30 22:55:08 +01:00
Edwin Brady
b0e55b53eb A bit more library support 2020-03-30 13:06:59 +01:00
Matus Tejiscak
fcdfa8e191 Fix comment. 2020-03-29 19:50:43 +02:00
Matus Tejiscak
9154a9b02b Add comments. 2020-03-29 19:48:00 +02:00
Matus Tejiscak
2b264d0517 Make sortBy stable. 2020-03-29 19:38:54 +02:00
Marshall Bowers
5b1e8bf436 Add intercalate for Data.List 2020-03-28 13:18:51 -04:00
Matus Tejiscak
d819bf5a9d Fix SeqEmpty in Text.Lexer.Core. 2020-03-28 15:02:08 +01:00
Edwin Brady
d666ed50c9 A couple of library functions 2020-03-19 22:14:48 +00:00
Edwin Brady
dd7ed89ed0
Merge pull request #222 from ziman/sorted-map-set
Adapt Data.Sorted{Map,Set} from Idris 1
2020-03-18 20:35:33 +00:00
Edwin Brady
6f933ba230
Merge pull request #221 from ziman/parser-lazy
Make the applicative combinators in `Text.Parser.Core` lazier
2020-03-18 20:35:01 +00:00
Edwin Brady
8b6527867a
Merge pull request #220 from ziman/lexer-parser-core
Add Text.{Lexer,Parser}.Core to the list of installed modules
2020-03-18 20:34:30 +00:00
Edwin Brady
b5b9372fff Add delete and union to Data.List 2020-03-10 14:52:46 +00:00
Edwin Brady
5bc11e4698 Add 'new1' to Control.App
Sometimes useful in App1 programs to add new state.
2020-03-09 21:23:56 +00:00
Matus Tejiscak
4dc0625237 Adapt Data.Sorted{Map,Set} from Idris 1. 2020-03-08 22:03:32 +01:00
Matus Tejiscak
9f793c31aa Change Lazy to Inf. 2020-03-08 20:53:39 +01:00
Matus Tejiscak
a32d1ca50f Make the applicative combinators in Text.Parser.Core lazy. 2020-03-08 20:35:08 +01:00
Matus Tejiscak
952d5c3c00 Add Text.{Lexer,Parser}.Core to the list of installed modules. 2020-03-08 20:23:27 +01:00
Edwin Brady
25843793c7 Improve linearity in Control.App
There are a few things that have linear usage but wasn't explicit in
types, so this will make some things easier to use in linear protocols.
2020-03-08 12:53:59 +00:00
Edwin Brady
34044597c0
Merge pull request #213 from ska80/prelude/getchar-putchar
Add getChar, putChar and putCharLn to prelude
2020-03-07 14:15:22 +00:00
Edwin Brady
9060b24f2f Move network test to chez test suite 2020-03-05 18:03:12 +00:00
Edwin Brady
67dc71f3c9
Merge pull request #208 from ska80/network-test
Simplify 'test' target in libs/network/Makefile
2020-03-05 10:30:18 +00:00
Edwin Brady
aef66099b5
Merge pull request #207 from ska80/update-gitignore
Improve .gitignore patterns
2020-03-05 10:29:11 +00:00
Kamil Shakirov
c8c0c5fb49 Add getChar, putChar and putCharLn to prelude 2020-03-05 14:55:20 +06:00
Kamil Shakirov
30830de5b7 Simplify 'test' target in libs/network/Makefile 2020-03-02 16:27:55 +06:00
Kamil Shakirov
d3820e1197 Improve .gitignore patterns 2020-03-02 14:21:43 +06:00
Edwin Brady
a5c356f998 Basic support for struct in FFI
Just in the Chez backend for now, and not allowing strings or functions
due to limitations of Chez.
2020-03-01 23:23:21 +00:00
Edwin Brady
b83f01e2f4 Small documentation updates 2020-02-28 00:15:03 +00:00