edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity
1,284 Commits 2 Branches 1 Tag 4.2 MiB
master
Commit Graph

50 Commits

Author SHA1 Message Date
Edwin Brady
c0b7c6a9d8
Merge pull request #367 from cypheon/bugfix/ttc-bigint-unmarshalling 
Fix unmarshalling of Integer values in TTC (Fixes: #345)
 2020-05-19 19:38:15 +01:00
Edwin Brady
c197c0f777 Update Buffer+File libraries 
Adding primitives - it's useful to distinguish between 32 bit and 64 bit
integers when writing to buffers.
 2020-05-19 16:06:05 +01:00
Edwin Brady
4c35210025
Merge pull request #370 from ska80/fix-makefiles 
Refactor makefiles
 2020-05-16 17:34:51 +01:00
Johann Rudloff
735395f403 Fix expected values of arithmetic test 
These are the correct results, verified by performing the calculations
"manually" in both Python 3 and Chez Scheme.
 2020-05-15 15:48:57 +02:00
Kamil Shakirov
109feaaf2f Fix tests/chez/chez017 test 2020-05-15 16:03:34 +06:00
Edwin Brady
dc67515611 Fix and test directory code 2020-05-14 12:40:48 +01:00
Kamil Shakirov
982629509b Merge branch 'master' into fix-makefiles 2020-05-13 16:25:15 +06:00
Kamil Shakirov
2ad471a5e3 Refactor makefiles to use some common options 2020-05-13 16:23:07 +06:00
Edwin Brady
1b36dd99b1 Move putChar, getChar etc primitives to C 
Back ends can still shortcut these and use their own primitives, but
doing things this way gives consistent behaviour between the simple IO
primitives and file IO, and allow us to use stdin/stdout consistently
(e.g. to flush stdout).
This also fixes the behaviour of 'replWith' to be consistent with the
Idris 1 version.
 2020-05-13 11:09:05 +01:00
Kamil Shakirov
8261b361e0 Merge branch 'master' into fix-makefiles 2020-05-13 09:05:29 +06:00
Edwin Brady
38e43f2c17 Move file management to C support library 
This removes the need for some external primitives, and allows the
details to be shared between all the backends (plus we don't have to do
things a certain way just because Scheme chooses to)
 2020-05-12 22:35:14 +01:00
Kamil Shakirov
1c8036dc58 Fix building shared libraries with correct extensions 2020-05-12 20:34:49 +06:00
Edwin Brady
9328579575 Hack for optimising some enumerations 
Really this should be generalised to any type that looks like an
enumeration after erasure, but this catches the most common options
quickly.
 2020-05-11 18:10:08 +01:00
Edwin Brady
7adb4d3342 Move buffer API to C 
It's slightly different wrt to file reading and writing, and now
requires the created buffer to be explicitly freed (since unlike Idris 1
the run time can't be told to manage C values) but this makes the buffer
code more portable by not requiring it to run via scheme.
Performance appears more or less the same as before.
 2020-05-11 18:10:08 +01:00
Christian Rasmussen
0694b6c0ef Update chez016 test to not rely on realpath 2020-05-09 23:19:38 +02:00
Christian Rasmussen
69aff544b6 Add test of noNewtype 2020-04-29 21:01:33 +02:00
Christian Rasmussen
2a3213d10a
Merge branch 'master' into fix-chez-in-folder-with-spaces 2020-04-21 15:01:01 +02:00
Edwin Brady
2b6000ecac Shuffle some tests around 
Making sure that tests which use chez are run after we've checked chez
is installed
 2020-04-21 12:03:49 +01:00
Christian Rasmussen
4d2b270db6 Allow spaces in file path for generated Chez programs 2020-04-18 18:18:02 +02:00
Arnaud Bailly
5544919c31 use quotient on scheme backends 
We compile divisions of Integers to quotient instead of '/' and add
some tests for numbers
 2020-04-15 10:52:35 +02:00
Edwin Brady
2938e86421 Ints in buffers are 32 bit 
...for consistency with Idris 1 (probably to be revisited later). So,
when working via the scheme primitives, we need to read/write 32 bits.
 2020-03-27 20:54:39 +00:00
Edwin Brady
59b66d6134 Add prettyName 
This is to display names in a user friendly way, especially case and
with block names
 2020-03-18 19:33:19 +00:00
Edwin Brady
9060b24f2f Move network test to chez test suite 2020-03-05 18:03:12 +00:00
Edwin Brady
fc0cfcb22b
Merge pull request #210 from ska80/chez010-test-makefile 
Use Makefile for tests/chez/chez010
 2020-03-05 10:31:45 +00:00
Kamil Shakirov
ac827222e8 Use Makefile for tests/chez/chez010 2020-03-03 18:11:47 +06:00
Kamil Shakirov
b14559c08c Use Makefile for tests/chez/chez013 
Fixes running tests on MacOS where dlopen(3) loads shared libraries with 'dylib' extension.
 2020-03-03 14:57:45 +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
2465e5a149 Some buffer updates 
Initialising buffers from files, error checking on creation, resizing.
 2020-01-31 16:49:31 +00:00
Edwin Brady
bb6cefc0a9 Added Data.IOArray 
plus scheme primitives for runtime, via vectors
 2020-01-30 17:04:33 +00:00
Edwin Brady
3cb574102a Add idiom brackets 2020-01-26 17:24:25 +00:00
Edwin Brady
1da3af5b2a Add ! notation 
In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
 2020-01-26 16:52:25 +00:00
Edwin Brady
04e4ebf80e Better approach to erasure in pattern matching 
It's a big patch, but the summary is that it's okay to use a pattern in
an erased position if either:

- the pattern can also be solved by unification (this is the same as
  'dot patterns' for matching on non-constructor forms)
- the argument position is detaggable w.r.t. non-erased arguments, which
  means we can tell which pattern it is without pattern matching

The second case, in particular, means we can still pattern match on
proof terms which turn out to be irrelevant, especially Refl.

Fixes #178
 2020-01-21 18:47:43 +00:00
Ilya Rezvov
32b1c9b34f use an explicit extension for libcb references in %foreign pragmas 2020-01-09 11:55:33 -08:00
Ilya Rezvov
b437323fd2 dylib extension added for libcb to fix chez010 test on MacOS 2020-01-01 14:23:02 -08:00
Edwin Brady
bf5b2298e0 Update test chez010 
To use expressions to calculate FFI convention, so that it's tested.
 2019-12-30 21:16:07 +00:00
Michael Morgan
e6121e0935 Remove trailing whitespace from Idris sources. 
This is the result of running the command:

$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +

I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
 2019-10-25 14:24:25 -07:00
Edwin Brady
85459814ef Support foreign callbacks in Racket back end 2019-09-29 19:37:30 +01:00
Edwin Brady
c6039e4fe5 Support callbacks in foreign calls to C 
Currently Chez backend only
 2019-09-29 17:25:26 +01:00
Edwin Brady
78e44a4353 Reading/writing buffers can fail 
So, make them return and Either and wrap the scheme definitions in an
exception handler that returns an error code on failure
 2019-09-28 18:33:46 +01:00
Edwin Brady
1a4f424259 Support UTF8 strings 
When writing to ttc, need to take the length in bytes rather than the
length in characters. Also need to write to scheme in the appropriate
format for each scheme system.

While we're at it, Idris 1 supports unicode identifiers (although we
don't encourage it :)) so this allows any characeter >127 in an
identifier.
 2019-09-28 14:08:23 +01:00
Kamil Shakirov
0722b96fef Add '--no-banner' option 2019-09-24 20:26:25 +06:00
Arnaud Bailly
2f8daa7cf2 Merge branch 'master' of https://github.com/edwinb/Idris2 into add-version-command 2019-09-22 22:39:36 +02:00
Arnaud Bailly
9c1f8b6f02
Merge branch 'master' into add-version-command 2019-09-22 15:50:13 +02:00
Edwin Brady
9b639eee35 Nat optimisation needs to look under lambda 
Names are saturated, so there might be a lambda in the term we're
optimising. Fixes #62
 2019-09-18 10:00:30 +01:00
Arnaud Bailly
558776c4c4
remove version number from banner at REPL startup 
otherwise all tests will need to change every time version changes...
 2019-08-29 14:37:04 +02:00
Edwin Brady
f37da6c5b7 Start adding tests for TypeDD book 
Also detailing any changes needed to the code. Added primitives for
Doubles, and repl/replWith to get Chapter 2 code to work.
 2019-06-30 15:50:58 +01:00
Edwin Brady
2f4cdf857d Make typecase on -> work 2019-06-29 22:43:06 +01:00
Edwin Brady
f9ea1ff329 Updating typecase, add tests 2019-06-29 21:32:19 +01:00
Edwin Brady
7b504e7a9e More Chez tests 2019-06-25 21:27:46 +01:00
Edwin Brady
69199639cf Fix Nat hack 
And add chez scheme section to tests, with one initial test
 2019-06-25 14:05:54 +01:00