russoul
0824e93874
Add more defs and comments into the test file
2020-10-03 19:26:21 +03:00
Ruslan Feizerahmanov
2e627ad16e
Remove invalid implicit in PreorderReasoning ( #727 )
2020-10-03 14:53:14 +01:00
G. Allais
5e85446e9c
[ fix #724 ] Typo in the magic string ( #726 )
2020-10-03 14:39:13 +01:00
russoul
5061b9f84d
Make logging lazy (logC)
2020-10-03 14:17:45 +03:00
russoul
273b71c632
Clean up
...
Fix #725
2020-10-03 14:01:42 +03:00
russoul
98bfff4a27
Merge branch 'master' of https://github.com/idris-lang/Idris2 into master
2020-10-03 11:51:48 +03:00
russoul
d49bf75eac
Clean up
2020-10-03 11:50:38 +03:00
Ohad Kammar
c02481fb55
[contrib] Add a Reflects
datatype ( #722 )
...
* [contrib] Add a `Reflects` datatype
as discussed in PR #695
2020-10-02 17:41:36 +01:00
G. Allais
f17354a503
Fix link in feature-requests-and-proposals.md
2020-10-02 14:40:22 +01:00
G. Allais
4a61146ba0
[ fix #705 ] Normalise primitives in mkPat ( #718 )
...
[ log ] prettier log for pats & clauses
[ re #650 ] Even lazier
[ fix #705 ] normalise primitives in mkPat
[ refactor ] introduce getPrimitiveNames
2020-10-02 12:22:57 +01:00
russoul
a667aae797
Fix another DPair parsing regression
2020-10-02 11:22:48 +01:00
zenntenn
f9880a31e4
Update CONTRIBUTING.md
2020-10-01 13:26:36 -04:00
MarcelineVQ
1619206d24
add specifier check for cli compilation
...
Missed a case which is covered now by checking for exceptions where
postOptions is used
add *> <* to Core
2020-10-01 14:12:31 +01:00
Molly Miller
7d5ec53b53
Add a (>>) operator, implemented in terms of (>>=).
...
This mirrors the (>>) found in Haskell, which is the same as (>>=), except the
second computation (on the right hand side) takes no arguments, and the result
of the first computation is discarded. This is a trivial implementation written
in terms of (>>=).
2020-10-01 13:16:58 +01:00
Molly Miller
dff0f1da43
network: Retrieve AF_* magic constants from C support code.
...
The Network.Socket.Data code previously used hardcoded constants manually read
from auto-generated C source code, however these constants are specific to
Linux. The original code looked like this:
export
ToCode SocketFamily where
-- Don't know how to read a constant value from C code in idris2...
-- gotta to hardcode those for now
toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
toCode AF_UNIX = 1
toCode AF_INET = 2
toCode AF_INET6 = 10
The AF_INET6 constant is correct on my Debian 10 laptop:
molly on flywheel ~> grep -rE '^#define AF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define AF_INET6 PF_INET6
molly on flywheel ~> grep -rE '^#define PF_INET6' /usr/include
/usr/include/x86_64-linux-gnu/bits/socket.h:#define PF_INET6 10 /* IP version 6. */
However, this is not the case on an OpenBSD machine:
spanner# grep -rE '^#define[[:space:]]+AF_INET6' /usr/include
/usr/include/sys/socket.h:#define AF_INET6 24 /* IPv6 */
This commit adds accessor functions to the C runtime support library for
retrieving the values of these macros as they appear in the system libc header
files, which can then be invoked using the normal C FFI machinery.
2020-10-01 12:05:42 +01:00
russoul
cf956ec09d
Remove whitespace
2020-10-01 12:49:59 +03:00
russoul
b57b28a64e
Implement new application syntax
...
Add syntax for bind-all-explicits
Add new record update syntax
Remove PInstance
2020-10-01 12:43:43 +03:00
Brandon Elam Barker
28cf2a3083
Making "functional dependencies" easier to find
2020-09-30 19:33:02 +01:00
Rodrigo B. de Oliveira
a7cf1143b6
Make NmLet
names unique in Compiler.ES.Imperative
...
Since the imperative form has no nesting of scopes.
Fixes #643
2020-09-30 13:43:59 +01:00
Arnaud Bailly
85f5d00054
fix totality annotation on some Nat functions
2020-09-30 10:51:51 +01:00
Ruslan Feizerahmanov
1d99a28176
Add Bifunctor interface ( #701 )
2020-09-30 10:51:07 +01:00
russoul
af62955e07
Merge branch 'master' of https://github.com/idris-lang/Idris2 into master
2020-09-29 12:58:28 +03:00
Niklas Larsson
5bbbfaf225
Merge pull request #709 from melted/unix_lib
...
Put the appdir first in LD_LIBRARY_PATH
2020-09-28 21:54:25 +02:00
Niklas Larsson
d5393b93bd
Put the appdir first in LD_LIBRARY_PATH
...
So that we prefer the local support lib before others in the path.
2020-09-28 21:02:48 +02:00
MarcelineVQ
3f105cdc0f
revert binary character literal
...
this wasn't doing anything anyway as it's first handled while
escaping in src/Parser/Support.idr and ends up clashing with \b
2020-09-28 13:25:03 +01:00
G. Allais
3df1f9c476
[ fix #63 ] interleaving let binders and local declarations ( #691 )
2020-09-28 13:15:22 +01:00
Guillaume ALLAIS
416b9578e5
[ fix #37 ] Use filename if we already know it
2020-09-24 15:56:23 +01:00
Guillaume ALLAIS
0d08c0b81b
[ log ] for desugaring of idioms
2020-09-24 15:27:40 +01:00
MarcelineVQ
961a28ee64
fix idiom brackets to account for IAlternative
...
Things like (,) () aren't straightforward IVar's but are IAlternative's
which present options about how the term should resolve. [| |] was not
accounting for this.
2020-09-24 15:27:40 +01:00
MarcelineVQ
315fc8ce2d
change ForeignFn to use TTImp to match RawImp version
2020-09-24 09:00:00 +01:00
Guillaume Allais
6d8bd62795
[ cleanup ] we only need one ifThenElse
2020-09-23 22:20:45 +01:00
Guillaume ALLAIS
cc31076849
[ test ] more corner cases
...
Making sure the test can distinguish between truncating & rounding.
2020-09-23 19:48:58 +01:00
Guillaume ALLAIS
621a9202ed
[ test ] making sure cast works
2020-09-23 19:48:58 +01:00
russoul
883a8df429
Fix String->Int cast on Scheme backends
2020-09-23 19:48:58 +01:00
Christian Rasmussen
091465525b
Remove FArgList
2020-09-23 18:33:19 +01:00
Brandon Elam Barker
9aefc9f60c
Updating info about backends in FAQ
2020-09-23 18:32:46 +01:00
G. Allais
d105dd11a7
[ breaking ] remove List1 related ambiguities ( #690 )
2020-09-22 15:07:40 +01:00
Jan de Muijnck-Hughes
8adfefa4e5
Added some logging information to the totality checker. ( #679 )
2020-09-22 12:44:13 +01:00
Ohad Kammar
e77b9b4631
[minor] Make base/Data.Nat.divNatNZ
compile-time reducible ( #689 )
...
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
2020-09-22 09:53:05 +01:00
MarcelineVQ
c4abdb4480
add Semigroup for Ordering and a -> b
...
useful items for applying multiple predicates, e.g.
sortBy (comparing length <+> compare)
To sort some lists elements by length and then lexographically
2020-09-21 08:07:21 +01:00
Matus Tejiscak
cf45f43f4e
Move the Buffer struct back into the .c file.
2020-09-20 17:49:25 +02:00
Christian Rasmussen
9add729ca3
Add Data.String.Iterator implementation for JavaScript
2020-09-20 17:44:19 +02:00
Matus Tejiscak
0a203f8f52
Add a warning comment.
2020-09-20 17:42:50 +02:00
Matus Tejiscak
b58cc433c8
Index StringIterator with the String it refers to.
2020-09-20 10:36:04 +02:00
Matus Tejiscak
d26a9c55bf
Tune Data.String.Iterator.
2020-09-20 10:02:18 +02:00
Matus Tejiscak
f73fa55075
Unpack strings into a lazy list.
2020-09-19 22:48:45 +02:00
Matus Tejiscak
e36c211cc0
Add a missing covering
annotation.
2020-09-19 21:57:54 +02:00
Matus Tejiscak
74f592053e
Make StringIterator abstract.
2020-09-19 21:54:34 +02:00
Matus Tejiscak
e73c6ae3c6
Add comments to fastUnpack and fastConcat.
2020-09-19 19:19:09 +02:00
G. Allais
8d09ec9c93
[ new ] comma-separated interface parameters ( #682 )
2020-09-19 15:29:23 +01:00