Steve Dunham
9646b31f2b
[ test ] Fix timing issue in interactive045 test
2022-09-06 10:05:34 +01:00
Steve Dunham
90e46ef340
Add test case for lexer issue and fix other instance.
2022-09-05 13:47:41 -07:00
G. Allais
ece1198074
[ fix #1742 ] Do not use uppercase names as pattern variables ( #2642 )
2022-09-05 12:45:51 +01:00
Steve Dunham
351b5ba720
[ parser ] Fix issue where Alt drops incoming commit tag
2022-09-05 12:44:02 +01:00
Steve Dunham
2e45902048
[ parser ] Better error messages inside if statements.
2022-09-05 12:44:02 +01:00
Steve Dunham
150673622b
[ test ] Add a sleep 1 to the interactive044 test to work around a race condition
2022-09-04 09:17:22 +01:00
Guillaume Allais
f678043854
[ test ] add tricky test case ported from Agda
2022-09-02 16:06:40 +01:00
Guillaume Allais
552f27f813
[ fix #2640 ] Do not shadow function name during case split
2022-09-02 11:55:15 +01:00
Guillaume Allais
6891490ed2
[ fix ] support for implicits in Deriving.Functor
...
A lot of refactoring to bring these. That's hopefully the last
feature that was needed...
2022-08-29 18:35:24 +01:00
Mathew Polzin
23e3695d74
Add test for auto implicit case splitting.
2022-08-16 09:23:19 +02:00
Zoe Stafford
86c060ef13
Reimplement %nomangle in terms of %export ( #2604 )
...
* Reimplement %nomangle in terms of %export
Also deprecate %nomangle
* [ lint ] fix linter errors
2022-08-15 13:26:06 +01:00
Guillaume Allais
4672305fc3
[ fix ] more filtering of invalid datatypes
2022-08-13 11:29:19 +01:00
Nil Geisweiller
719b5ad17f
[ cleanup ] Remove extraneous show and simplify printLn ( #2618 )
2022-08-10 21:22:58 +01:00
Justus Matthiesen
a30209d492
[ fix ] Remove stray ")" in Show instance for Term ( #2611 )
2022-08-08 15:24:07 +01:00
Steve Dunham
f4dc7f4221
Merge branch 'main' into issue-2557
2022-08-03 07:13:04 -07:00
Steve Dunham
4088dd863b
Rebuild TTC if they don't contain needed incremental data (related to #2560 )
2022-08-03 07:12:46 -07:00
Guillaume Allais
a4b99bd81c
[ refactor ] introduce allSemanticHighlighting
...
Side effect: all the aspects are now sorted by ranges as we are
merging the PosMaps instead of appending the lists.
2022-07-19 15:01:20 +01:00
G. Allais
84a504738c
[ doc ] add comments to generated javascript ( #2594 )
2022-07-18 17:30:56 +01:00
Guillaume Allais
8ecb1aaf95
Revert "Fix issue with case inside a type."
...
This reverts commit 50ca28c068
2022-07-18 15:58:29 +01:00
Steve Dunham
50ca28c068
Fix issue with case inside a type.
2022-07-18 14:17:14 +01:00
G. Allais
0cbbf97b79
[ new ] extend Deriving.Functor to (non-strictly) positive functors ( #2591 )
2022-07-18 14:10:46 +01:00
Mathew Polzin
4a348c1f95
Public export remaining function to allow for proofs involving parsing numbers.
2022-07-18 14:10:05 +01:00
Steve Dunham
a0d9e2bbba
Update tests using base64 utility to also work on macos ( #2536 )
...
* Update tests using base64 utility to also work on macos
* Fix invocation of base64 in refc/buffer test.
2022-07-13 06:46:31 -07:00
G. Allais
1f41c8b44d
[ close #647 ] Already fixed ( #2581 )
2022-07-08 14:16:25 +01:00
Guillaume Allais
ac2ef882f6
[ fix #2573 ] Solve constraints before looking at eq type
2022-07-07 20:36:05 +01:00
Guillaume Allais
19bc798952
[ re #2526 ] Update golden value
2022-07-07 20:34:54 +01:00
Guillaume Allais
d19dbfffff
[ fix #2229 ] better warning
2022-07-07 16:42:34 +01:00
G. Allais
4874bf2114
[ fix ] handle implicit arguments in Deriving.Functor ( #2572 )
2022-07-07 09:55:13 +01:00
Stefan Höck
5a962929e7
[ fix ] issue 2537 ( #2538 )
...
Co-authored-by: Zoe Stafford <zoepolarsax@gmail.com>
2022-07-07 09:54:52 +01:00
Guillaume Allais
7db20d38a3
[ cleanup ] Fewer assert_total in deriving Functor
2022-07-04 12:03:49 +01:00
G. Allais
aeeb338e6c
[ new ] deriving Functor ( #2568 )
2022-07-04 08:58:18 +01:00
Ruslan
dbba32ea09
Fix an eta issue in elaborator-reflection ( #2449 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Denis Buzdalov <public@buzden.ru>
2022-06-30 22:01:31 +01:00
Steve Dunham
0454dfd66a
Address issue #2557 Incremental compilation is used when .so files are missing.
2022-06-25 19:56:56 -07:00
G. Allais
4024857d20
[ base ] Various Language.Reflection improvements ( #2554 )
2022-06-22 13:07:27 +01:00
Guillaume Allais
e5802204b6
[ fix ] holes in record types
2022-06-17 10:17:40 +01:00
Guillaume Allais
2060535d08
[ new ] name hints for primitive types
2022-06-14 16:07:37 +01:00
Guillaume Allais
7bd7f1da9c
[ fix ] resugaring of DPair
2022-06-08 22:44:55 +01:00
György Kurucz
79a2f677d4
[ re #1282 ] Improve unelaboration of case expressions
2022-06-08 17:01:36 +01:00
Zoe Stafford
b9001439b3
Revert "Transitive dependencies v2 ( #2496 )"
...
This reverts commit 51f952714d
2022-06-08 06:35:39 +01:00
Zoe Stafford
51f952714d
Transitive dependencies v2 ( #2496 )
...
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
* Actually install the version
This should make things start working
2022-06-07 14:31:14 +01:00
G. Allais
5e9a90bd97
[ fix ] semantic highlighting in IDE mode ( #2509 )
...
* [ fix ] semantic highlighting in IDE mode
Bring back (?) highlighting of goals
* [ debug ] better logging: add length
* [ test ] turns out lengths are not needed!
2022-05-28 11:23:07 +01:00
Denis Buzdalov
599027a893
[ fix ] Make able to interpret result of a macro as a function
2022-05-27 09:36:44 +01:00
Xerz
e9f562f435
[ prelude ] Add Range implementation for Char ( #2505 )
2022-05-27 07:57:59 +01:00
G. Allais
607a2a2110
[ IDE ] refine command ( #2490 )
2022-05-25 11:29:03 +01:00
Zoe Stafford
932a24baa1
Revert "make depends collect all transitive dependencies ( #2469 )"
...
This reverts commit fde6269c7e
2022-05-21 06:49:07 +01:00
Zoe Stafford
fde6269c7e
make depends collect all transitive dependencies ( #2469 )
...
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
2022-05-20 16:20:54 +01:00
G. Allais
fdbd858d97
[ refactoring ] expose some internals needed by Katla ( #2480 )
2022-05-16 20:37:08 +01:00
Joel Berkeley
bf87b623ef
add scanr; scanr1; unsnoc for Vect ( #2471 )
...
* add `scanr` and `scanr1` for `Vect`
* add tests
* tests
* docstring
* typos
* add unsnoc
* simplify unsnoc
* docstring
* typos
2022-05-12 17:54:34 +01:00
Guillaume Allais
7c784dd89c
[ fix ] missing rigs in doc type signatures
2022-05-12 10:25:54 +01:00
G. Allais
f80fc184e3
[ new ] :exec for RefC ( #2466 )
2022-05-10 15:09:53 +01:00
Jesse Nava
db13a35bf5
[ fix ] Ensure casting from String to Double results in floating numbers on scheme backends
2022-05-09 18:36:17 +01:00
György Kurucz
7a5f63eab0
[ fix ] Add missing cases for BITS types in extractInt
...
e79e4277Fixes #2452
2022-05-04 10:18:58 +01:00
G. Allais
4256cd15fd
[ highlighting ] case trees in :di ( #2440 )
2022-04-29 12:52:23 +01:00
Steve Dunham
04e65529f6
Better parse error for missing paren after with
2022-04-29 08:59:40 +01:00
vfrinken
b1f45f2748
RefC backend improvements ( #2425 )
...
* RefC backend improvements
1. OnCollect had the wrong number of arguments. The code creator expects
3 arguments, but onCollect in prim.h expected 4 arguments. The first of which
was an erased arguments. That is now fixed.
2. OnCollect did not call `newReference` when creating a new reference to the pointer
and the freeing function
3. OnCollect and OnCollectAny still had a spurious printf statement
Those issues have been fixed, the test case can be found in
tests/refc/garbageCollect
4. The IORef mechanism expects that the %World token will be passed around
consistently. This is not the case. States in Control.App make use of
IORefs, but the function created from Control.App.prim_app_bind
had the world token erased to NULL.
Now, IORefs are managed using a global variable,
IORef_Storage * global_IORef_Storage;
referenced in cBackend.h, defined in the created .c file, and set to NULL
in main();
5. While multithreading and forking is still not supported, compiling a program
that makes use of Control.App demands a C implementation of prim_fork.
Files support/refc/threads.c and support/refc/threads.h provide a
dummy implementation for it, so that Control.App programs compile and run.
A test for these 2 issues is given in tests/refc/issue2424
* format changes
to make the linter happy
* format changes
to make the linter happy
* format changes
to make the linter happy
* spelling mistake braket -> bracket
Co-authored-by: Volkmar Frinken <volkmar@onutechnology.com>
2022-04-27 13:59:32 +01:00
G. Allais
05baf44b5b
[ refactor ] Index Pretty over the type of annotations ( #2371 )
2022-04-27 12:26:59 +01:00
Guillaume Allais
81ba322a4b
Revert "[ fix ] search should solve auto implicits before implicits"
...
This reverts commit 6dd68e8924#2437
2022-04-27 11:00:51 +01:00
Guillaume Allais
6dd68e8924
[ fix ] search should solve auto implicits before implicits
2022-04-26 15:07:51 +01:00
G. Allais
22b98f231e
[ fix ] highlight unambiguous names in `with' ( #2423 )
2022-04-22 13:34:05 +01:00
G. Allais
98b1062772
[ fix ] :printdef support for P(D)Pair & Equal ( #2416 )
2022-04-15 20:39:46 +01:00
Guillaume Allais
ec4cf3d48c
[ fix ] pretty printing of misspellings
2022-04-15 20:18:48 +01:00
Guillaume Allais
0986cf177b
[ parse ] better error message for list literals
...
I got fed up with being puzzled whenever edwin's trailing commas
and my leading commas clash and the error location is the opening
square bracket rather than the repeated comma.
2022-04-15 11:33:20 +01:00
Guillaume Allais
b4662a8537
[ fix ] show keywords & bound variables
2022-04-14 12:17:11 +01:00
Guillaume Allais
e0f5f541e2
[ fix #2402 ] Check totality before exiting failing block
2022-04-08 13:21:46 +01:00
Guillaume Allais
55d6c50706
[ fix ] make 'failing' whitespace-insentitive
2022-04-07 13:59:27 +01:00
Mathew Polzin
c91a768486
System NodeJS additions ( #2401 )
2022-04-07 10:09:30 +01:00
G. Allais
79e733b848
[ new ] multi-with elaborated as nested withs ( #2403 )
2022-04-07 09:30:23 +01:00
Thomas E. Hansen
a644a85a57
[ base ] public export quantifier functions
2022-04-04 13:24:12 +02:00
G. Allais
4b6936d615
[ fix ] allow refined implicit patterns in with clauses ( #2393 )
2022-04-03 10:45:29 +01:00
Guillaume Allais
ad78457869
[ fix ] location information in with clauses
2022-04-01 11:41:48 +01:00
Guillaume Allais
bc9a319ddf
[ parser ] bunched args in implementation implicits
2022-03-31 15:46:44 +01:00
Denis Buzdalov
2538b1e82b
[ syntax ] Require indent for blocks like mutual and failing ( #2387 )
2022-03-31 12:54:38 +01:00
Denis Buzdalov
03f23b0457
[ error ] Improve the indented non-empty block's error message
2022-03-31 10:44:06 +01:00
Guillaume Allais
921d3b7b50
[ parser ] better error messages for Haskellers
2022-03-31 10:43:46 +01:00
Zoe Stafford
8c7fc581c6
Fix prim__div_Double on Node/js backend
...
problem was found by @kuruczgy on the idris discord
Also add tests
2022-03-26 19:00:46 +00:00
G. Allais
2aa0069e63
[ doc ] also display definition's visibility ( #2374 )
2022-03-24 23:11:10 +00:00
Denis Buzdalov
e8d3d788c1
[ base ] Add some more properties, functions and interface implementations ( #2361 )
2022-03-23 13:33:13 +00:00
Giuseppe Lomurno
f38feaa48d
Clean path in more Core.Directory functions
2022-03-23 12:49:36 +00:00
G. Allais
35b2362487
[ new ] failing blocks ( #2360 )
2022-03-23 12:01:13 +00:00
Ohad Kammar
319c7f7b86
Move Syntax.PreorderReasoning into base ( #2368 )
2022-03-22 20:58:36 +00:00
G. Allais
0dfa7d8d79
[ doc ] prettier :di ( #2356 )
2022-03-18 08:45:18 +00:00
Joel Berkeley
fc45f7d888
[ base ] add insertAt for List ( #2336 )
2022-03-17 18:23:47 +00:00
Denis Buzdalov
05d64483f6
[ refactor ] Factor out a type for primitive types out of Constant
2022-03-10 23:07:20 +00:00
Guillaume Allais
14f2196d15
[ doc ] return module header docs
2022-03-09 13:31:30 +00:00
stefan-hoeck
51eb854a60
[ fix ] euclidian mod and div for scheme backends
2022-03-08 17:40:29 +00:00
stefan-hoeck
405f80946b
[ fix ] euclidian div and mod for JS backend
2022-03-08 17:40:29 +00:00
G. Allais
1c396744d9
[ doc ] :printdef for interface implementations ( #2340 )
2022-03-07 11:47:20 +00:00
Joel Berkeley
0ab0ecb199
add replaceAt for List ( #2335 )
2022-03-03 23:40:18 +00:00
Joel Berkeley
f436388a6b
adopt backend implementations of pow ( #2334 )
2022-03-03 23:39:25 +00:00
Jan de Muijnck-Hughes
4ba3bb6670
[ fix ] Literate things ( #2312 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-02-18 11:29:52 +00:00
Balazs Komuves
3345460fe9
[ fix #2176 ] Records in where-blocks are in the wrong namespace ( #2187 )
2022-02-16 15:43:50 +00:00
Joel Berkeley
5abc01453d
add deleteAt for List ( #2317 )
2022-02-11 09:28:36 +00:00
Guillaume Allais
bec4a0a88e
[ re #499 ] quantity-aware with-clauses
2022-02-09 09:19:40 +00:00
Robert Wright
1776efa8a5
Allow Type-level String operations
2022-02-03 16:10:47 +00:00
madman-bob
0ee9632e45
[ refactor ] Abstract Prelude.elem to work with all Foldables ( #2294 )
2022-02-01 21:34:29 +00:00
Stefan Höck
44245e1683
[ fix ] issue #2288 ( #2289 )
2022-01-28 09:01:09 +00:00
Stefan Höck
f1d56a4e0f
[ syntax ] Namespaced idiom brackets ( #2284 )
2022-01-24 16:18:36 +00:00
James Cook
e82600c4d6
[ opt ] transform rule making List.length tail-recursive. ( #2100 )
2022-01-24 16:12:29 +00:00
octeep
f137d96cd6
update refc/buffer to check how many bytes have been read
2022-01-24 15:58:32 +00:00
Mathew Polzin
35a84e505d
[ fix #2033 ] determining when to rebuild modules ( #2188 )
2022-01-21 10:26:20 +00:00
