Andy Lok
83ab4f0f15
Fix lint
2021-02-21 03:13:13 +08:00
Andy Lok
07eb6fda47
Allow hashtag escape for multi-line string
2021-02-21 03:11:01 +08:00
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