idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 08:42:11 +03:00
Code Issues Projects Releases Wiki Activity
1,407 Commits 6 Branches 9 Tags 113 MiB
fb77a3e043
Commit Graph

1407 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Rui Barreiro
30a190e0a2 re added replaceNamesExp 2020-10-05 15:11:22 +01:00
Rui Barreiro
44151ecbae Merge branch 'master' of github.com:idris-lang/Idris2 into issue_596 2020-10-05 14:47:17 +01:00
Rui Barreiro
a5b2247f28 mutual tail recursion 2020-10-05 14:39:38 +01:00
russoul
939de39a57 Rename stuff a bit 2020-10-03 19:44:12 +03:00
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