edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 22:52:25 +03:00
Code Issues Projects Releases Wiki Activity
452 Commits 2 Branches 1 Tag 4.2 MiB
4194409682
Commit Graph

70 Commits

Author SHA1 Message Date
Arnaud Bailly
4194409682 remove another message to make network tests more reliable 2019-09-13 18:43:35 +02:00
Edwin Brady
65db4fbf96 Put built ttcs in build/ttc, rather than build 
This is so that we can put other build artefacts (e.g. executables) in
properly organised subdirectories of build, e.g. build/bin/chez,
build/bin/js, etc.
 2019-09-04 12:41:16 +01:00
Edwin Brady
68b0d64879 Add parameterised pointer type 
For at least a bit of safety in foreign APIs. AnyPtr has the old Ptr
behaviour.
 2019-09-04 10:25:45 +01:00
Edwin Brady
bb246a072a Experimenting with a new FFI 
Functions can be declared as %foreign with a list of calling
conventions, which a backend will work through until it finds one it can
understand. Currently implemented only in Chez backend. If this works
out, I'll implement it for Racket too, and remove the old primitive
functions.

There's a bit more boiler plate here than before, but it has the benefit
of being more extensible and portable between different back ends.

Some examples, pending proper documentation:

%foreign "C:puts,libc" "scheme:display"
putline : String -> PrimIO ()

%foreign "C:exp, libm.so.6, math.h"
fexp : Double -> Double

%foreign "C:initscr, ncurses_glue.so, ncurses.h"
prim_initscr : PrimIO ()
 2019-09-02 17:10:48 +01:00
Edwin Brady
f123fcaf84 Display output on network test fail 
This still seems to be failing on travis, so let's see what it looks
like!
 2019-08-29 12:56:13 +01:00
Edwin Brady
6a0cfa125a Update network build test 
Since it's just to check that it's built successful and we can send a
message back and forth, remove the diagnostic message that might come
out in a different order depending on scheduling.
 2019-08-29 11:50:14 +01:00
Edwin Brady
ea75fd21a1 Merge branch 'master' of github.com:edwinb/Idris2 2019-08-29 11:10:44 +01:00
Edwin Brady
09b13eef21
Merge pull request #89 from chrrasmussen/fix-integerToNat 
Fixes #88: integerToNat hangs for negative integers
 2019-08-29 11:07:50 +01:00
Edwin Brady
02c5aa7b61
Merge pull request #76 from ska80/ignore-build-artifacts 
Ignore build artifacts
 2019-08-29 11:01:06 +01:00
Edwin Brady
8975eeafb7 Make a start on reflection 2019-08-27 15:49:21 +01:00
Edwin Brady
fb11b89a4e Make some things public export 
Anything which might appear in types should be! Fixes #93
 2019-08-21 17:44:17 +02:00
Christian Rasmussen
14db785ebe Fixes #88: integerToNat hangs for negative integers 2019-08-20 18:26:13 +02:00
Kamil Shakirov
a6f9fb5e18 Ignore build artifacts 2019-08-07 09:40:30 +06:00
Edwin Brady
0b692e4379 Pack/unpack should be public export 
They're likely to be useful when manipulating strings in proofs.
 2019-08-01 11:18:04 +01:00
Edwin Brady
89eb495d97 Merge branch 'network-lib' of https://github.com/abailly/Idris2 into abailly-network-lib 2019-08-01 11:11:45 +01:00
Arnaud Bailly
f66d681893
linked libraries should be after the source file referencing them 
http://gcc.gnu.org/onlinedocs/gcc/Link-Options.html
 2019-07-31 14:13:32 +02:00
Edwin Brady
47ad8ee7f5 Propagate implicits to with clauses 
Fixes #57. Also move much of the 'with' machinery to its own source
file.
 2019-07-30 12:32:33 +01:00
Arnaud Bailly
d600a3980c
added back missing file extension 2019-07-29 13:15:52 +02:00
Arnaud Bailly
ec402c3c4a
reference idris_net library as idris_net.so for all OSes 2019-07-29 12:46:23 +02:00
Arnaud Bailly
75459e7fca
fix execution of network test to correctly load library 2019-07-28 22:53:05 +02:00
Arnaud Bailly
f6b746e7ac
set LD_LIBRARY_PATH for network tests to run 2019-07-28 09:53:33 +02:00
Arnaud Bailly
02978c81fc
Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib 2019-07-27 17:27:49 +02:00
Arnaud Bailly
a87639d53a
refactor code to be more compact 
uses alternative branches for failed pattern matches in do-notation
 2019-07-26 09:51:49 +02:00
Arnaud Bailly
87b754de45
fix execution of tests to actually fail if there's an error 2019-07-25 19:49:15 +02:00
Arnaud Bailly
055a5f2449
got a first basic test passing 2019-07-25 09:43:33 +02:00
Alex Gryzlov
c3191f7d90 export decEq implementation 2019-07-24 17:13:47 +03:00
Alex Gryzlov
d289a0da4c fix names 2019-07-24 16:23:18 +03:00
Alex Gryzlov
b9b41dea40 port Data.List 2019-07-24 16:11:27 +03:00
Arnaud Bailly
b5cc727f3b
[wip] test basic server 2019-07-24 10:08:59 +02:00
Arnaud Bailly
dc219a07ec
provide a way to retrieve port of (server) socket bound to 0 2019-07-24 09:17:29 +02:00
Arnaud Bailly
7c1b1bc98d
got code to compile 
* removed Cgi
* add a couple of utility functions to the C source
* converted all foreign calls to use cCall
 2019-07-23 22:39:54 +02:00
Arnaud Bailly
2b11b7cc32
add test target and basic test 'harness' 
test harness is a grand word for just a basic C main file that uses
plain <assert.h> macro to run tests
 2019-07-23 09:38:28 +02:00
Arnaud Bailly
7f53d0d54d
add 'missing' functions into base libraries 2019-07-23 09:37:48 +02:00
Arnaud Bailly
18d83420da
initial import of idris 1 network lib 2019-07-22 17:24:55 +02:00
Edwin Brady
6dd18d798a Allow annotating functions with multiplicity 
This means we can write truly type level only functions, by annotating
them with a 0 before the type declaration.
 2019-07-20 18:04:18 +01:00
Edwin Brady
623024d179
Merge pull request #28 from jfdm/add-either 
Inclusion of Either within Base.
 2019-07-18 20:31:51 +01:00
Jan de Muijnck-Hughes
5823d6b294 Inclusion of Either within Base. 
Straightforward port of Either from Idris to Idris2.
 2019-07-18 16:32:19 +01:00
David Smith
96ec5f6b3a Add Data.Morphisms to base 2019-07-18 14:46:59 +01:00
Edwin Brady
b1081e6e04 Add missing export modifiers in Data.Vect 
Lots were missing, and some were export, which should probably be public
export because the nature of Vect is that it could commonly be used in
types.

Fixes #13
 2019-07-18 11:25:41 +01:00
Edwin Brady
4860d2b751 Add Range interface to prelude 
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
 2019-07-11 23:38:25 +02:00
Edwin Brady
fd4f90e331 Add some Control.Monad things 
This required a small change to auto implicit search (and I'm still not
sure about this). Now search arguments right to left, because solving
later arguments may resolve earlier arguments by unification and this
can happen in particular when chasing parent interfaces (which may have
fewer parameters).
 2019-07-10 20:18:40 +02:00
Edwin Brady
a422294f36 Pass auto implicits through interfaces 
This allows 'traverse' to work now (it was treating them as normal
implicits, so building the wrong form of application)
 2019-07-10 17:23:33 +02:00
Edwin Brady
2bb496f74b Chapter 11 examples now working 2019-07-08 23:46:20 +02:00
Edwin Brady
1cc097aefc Add Data.Primitives.Views 2019-07-08 22:11:34 +02:00
Edwin Brady
2967a19963 Add more stream functions to Data.Stream 2019-07-08 18:10:47 +02:00
Edwin Brady
11199acab6 Improve 'with' implementation 
Now supports with applications on the RHS when auto implicits are
involved. Auto implicit bound names in patterns now become searches on
the rhs in a with-application (I should write this construct up properly
in a paper some time!)
 2019-07-08 12:55:55 +02:00
Edwin Brady
ccc53813ca Initial attempt at RHS with application 
Still some details to finish, plus testing, plus adding View modules to
the base libraries, but the basic idea works.
 2019-07-07 00:07:59 +01:00
Edwin Brady
c02da23c1a Add sort and merge to Data.List 2019-07-06 13:56:57 +01:00
Edwin Brady
7a588d30cc Need to export DecEq implementations! 2019-07-05 18:41:50 +01:00
Edwin Brady
4ab543b83d A bit more library support, for Chapter 9 
Also a tweak to errors when compiling to scheme, so that it properly
reports an error then quits if it's supposed to crash.
 2019-07-05 17:24:15 +01:00