idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity
1,606 Commits 6 Branches 9 Tags 112 MiB
22a769e6b5
Commit Graph

1606 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Andy Lok
22a769e6b5 Implement multiline string 2021-02-20 18:05:26 +08:00
Guillaume ALLAIS
7ccc47712e [ re #1087 ] Better error messages in the REPL 
(as well as in type signatures now that I know how to do that)
 2021-02-19 12:34:19 +00:00
Guillaume ALLAIS
5b5bdfe769 [ contrib ] Positions in strings 
This is an alternative to using `fastUnpack` and `fastPack` to work
on lists of characters.

Using this to refactor the lexer and benchmarking the resulting
compiler on building idris2 shows it's 3 to 5s slower than the
current implementation that goes via `List Char`.

This may be backend-dependent so I still push this to contrib,
with the plan of running further benchmarks in the future.
 2021-02-18 17:52:25 +00:00
Mathew Polzin
d5d0b64b4a
withFile & writeFile cleanup (#1085) 2021-02-18 17:51:45 +00:00
Andy Lok
26464357c1
Implement interpolated string (#1056) 2021-02-18 13:07:22 +00:00
Mathew Polzin
9f8a8b5d76
Add a total way of reading files in. (#1070) 2021-02-18 11:13:25 +00:00
Nil Geisweiller
bb25050746 Remove redundant to 2021-02-18 09:56:42 +00:00
gemmaro
5eafe11de7 A tiny doc fix: the program name was idris 2021-02-17 09:30:52 +00:00
Stiopa Koltsov
1cf9de4021 Hide countFrom function from prelude 
`countFrom` must have been made public accidentally:
* it is defined in the ranges section of the file, not stream section
* it is used only in `Range` implementation
* the same function `iterate` is defined in `Data.Stream`

```
countFrom start next
```

is the same as

```
iterate next start
```
 2021-02-16 19:20:54 +00:00
Johann Rudloff
d86944fca2 Extract findDataFile code from readDataFile and export it 2021-02-16 19:16:07 +00:00
Kamil Shakirov
357e2a4cf6 Use double quotes to display the current working directory 2021-02-16 19:13:52 +00:00
Denis Buzdalov
b355b12cdb Some cleanup was done. Changed code is mosly equivalent to the former. 
A lot of useless matches of implicit arguments were removed.
 2021-02-16 19:05:33 +00:00
Guillaume ALLAIS
c2532acfd8 [ fix #1035 ] Not an internal error 2021-02-16 17:04:02 +00:00
Guillaume ALLAIS
e9f4dc5252 [ cleanup ] parser long lines 2021-02-16 17:04:02 +00:00
Stefan Hoeck
7401961425
[ new ] Bitwise XOR for Bits64 and Integer (#1026) 2021-02-16 15:14:56 +00:00
Denis Buzdalov
0ac34538ec A function from Not (x = y) to decEq x y = No _ was added. 2021-02-16 12:43:50 +00:00
Nil Geisweiller
f390fba766 Rename Sotrable to Storable 2021-02-16 09:51:44 +00:00
Alex Gryzlov
a1221fdbfd
Document new :l behaviour (#1061) 
Co-authored-by: Kamiλ Shakirov <ska80@users.noreply.github.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
 2021-02-15 18:56:05 +00:00
Dong Tsing-hsuen
447110c686 Fix typo in FC.idr. 
Change "beeen" to "been".
 2021-02-15 17:32:05 +00:00
André Videla
8c7a08f282
Merge pull request #1034 from andylokandy/lexer 
lexer: add a language-composable tokenizer
 2021-02-15 11:45:37 +00:00
Guillaume ALLAIS
059074fe14 [ test ] fix test suite output 2021-02-15 10:35:46 +00:00
Giuseppe Lomurno
440e60a00b Change PreorderReasoning arguments to 0 2021-02-15 10:35:46 +00:00
Denis Buzdalov
bd21fd51e2 Zero quantities were added to some interface usages. 2021-02-15 10:35:46 +00:00
Andy Lok
ed7ee4a57b Show more codes in error report 2021-02-15 10:35:46 +00:00
Michael Messer
0a76ab590e Generalize Category 2021-02-15 10:35:46 +00:00
G. Allais
301324b9b3 [ fix #1043 ] throw error if compileExpr failed (#1052) 
Also adding a CI target testing the gambit backend.
 2021-02-15 10:35:46 +00:00
russoul
1d23c7a6bd Add named instances for functor & applicative composition 2021-02-15 10:35:46 +00:00
G. Allais
a060dcc18e [ new ] Data.OpenUnion (#1050) 2021-02-15 10:35:46 +00:00
Z-snails
5384560009 [ new ] support record projections in refc backend (#1054) 2021-02-15 10:35:46 +00:00
Giuseppe Lomurno
70d1505c5c Change PreorderReasoning arguments to 0 2021-02-14 15:12:17 +00:00
André Videla
0705ba55c5 Refactor getFirstMatch function from tokeniser 2021-02-14 00:02:36 +00:00
Denis Buzdalov
4f28b92a19 Zero quantities were added to some interface usages. 2021-02-12 20:51:13 +00:00
Andy Lok
bb1edab3aa Show more codes in error report 2021-02-12 18:37:12 +00:00
Andy Lok
5cd7642991 Small improve 
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
 2021-02-12 14:01:12 +08:00
Andy Lok
4cd8cb5e75 Remove unused util 2021-02-12 13:20:07 +08:00
Andy Lok
99687976f4 Improve parse error report 
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
 2021-02-12 01:16:40 +08:00
Michael Messer
4baacc322b Generalize Category 2021-02-11 09:38:26 +00:00
G. Allais
399a2adb15
[ fix #1043 ] throw error if compileExpr failed (#1052) 
Also adding a CI target testing the gambit backend.
 2021-02-10 21:10:27 +00:00
russoul
b8aaaf3275 Add named instances for functor & applicative composition 2021-02-10 18:00:14 +00:00
Andy Lok
232c686e25 Improve doc 2021-02-10 23:52:00 +08:00
Andy Lok
b04ebe8cf1 Let lexer recognise grouping 
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
 2021-02-10 23:33:25 +08:00
G. Allais
8ba3d8572b
[ new ] Data.OpenUnion (#1050) 2021-02-10 15:25:35 +00:00
Z-snails
4eac2dd0b9
[ new ] support record projections in refc backend (#1054) 2021-02-10 14:46:41 +00:00
Andy Lok
b0dadebb22 Merge branch 'master' of https://github.com/idris-lang/Idris2 into lexer 2021-02-10 19:44:05 +08:00
Andy Lok
bec2e303ae Flattern Tokenizer 
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
 2021-02-10 19:43:09 +08:00
Stefan Hoeck
f721281bdc
[ re #1043 ] Fix typo in support.scm (#1047) 2021-02-10 01:00:42 +00:00
Guillaume ALLAIS
5aa4262792 [ fix ] some of the docs 2021-02-10 00:37:06 +00:00
Ohad Kammar
aa72203fc8
Preliminary datatypes for telescopes (#703) 
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-02-09 14:18:41 +00:00
Denis Buzdalov
123fbb7f33 weakenN's n parameter was made to have zero quantity. 2021-02-09 14:15:59 +00:00
Ohad Kammar
891b2d667a
[ fix ] All the REPL commands should be in CommandTable (#1036) 
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
 2021-02-08 17:25:49 +00:00