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