idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 04:09:10 +03:00
Code Issues Projects Releases Wiki Activity
3,054 Commits 6 Branches 9 Tags 115 MiB
542ebeae97
Commit Graph

3054 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Guillaume Allais
8b20da7e39 [ cleanup ] remove TT from base 
As discussed with edwin, let's get rid of the external TT type.
There is no way to get your hands on a TT value anyway so this
should not change anything.
 2022-07-07 16:42:19 +01:00
Denis Buzdalov
c03a39789f [ breaking ] Make arguments of runRWST like in other transformers 
Put the `RWST` argument to be the last one. This makes such functions
to be easier used in point-free compositions and to be easily
interchangeable with existing `runStateT`-like functions.
 2022-07-07 15:19:41 +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
Jeroen de Haas
ea7e43ad74 [doc] Remove implicit argument in documentation for parseDouble 2022-07-03 22:00:31 +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
Denis Buzdalov
38caff23b8 [ fix ] Make the result Show of case .. of compilable 
1. The arrow was fixed
2. Put explicit type ascription into a comment
3. Don't print type when it was not present in the expression
 2022-06-27 15:32:02 +01:00
Denis Buzdalov
afaa80a5ae [ re #2533 ] Fix printing of lazy values in Show TTImp 2022-06-27 15:32:02 +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
Denis Buzdalov
e856569d16 [ doc ] Clarify the doc comment of find* functions of SnocList 2022-06-20 12:13:37 +01:00
Denis Buzdalov
113085d0c3 [ base ] Add a function for changing the topmost FC of a TTImp 2022-06-17 19:53:07 +01:00
Denis Buzdalov
bc838467a3 [ base ] Add a function returning Dec for So 2022-06-17 19:52:35 +01:00
Justus Matthiesen
1ae4fdd605 Fix error message for LinearMisuse 2022-06-17 11:48:51 +01:00
Guillaume Allais
e5802204b6 [ fix ] holes in record types 2022-06-17 10:17:40 +01:00
Guillaume Allais
bf3272c344 [ minor ] more magic for name generation 2022-06-17 10:17:40 +01:00
Guillaume Allais
f111838e52 [ cleanup ] move TTC implementations to separate files 2022-06-17 10:17:40 +01:00
Denis Buzdalov
a7fb6722a0
[ re #2533 ] Fix recently added reflection's Show (#2543) 2022-06-16 11:08:51 +01:00
Denis Buzdalov
45579795bc [ elab ] Make any error in elab script to produce a special error type 2022-06-16 09:49:56 +01:00
Denis Buzdalov
742d41f696 [ elab ] Make actual bad script errors be reported so 2022-06-16 09:49:56 +01:00
Denis Buzdalov
df6f4f69cd [ doc ] Add clarification to the doc of a function of Elaboration 2022-06-16 09:49:56 +01:00
Denis Buzdalov
e590014fb7 [ cleanup ] Remove unused expression 2022-06-16 09:49:56 +01:00
G. Allais
bdf3833df5
[ new ] Auto in Agda (+ bonus) (#2541) 
* [ new ] Auto in Agda (+ bonus)

* [ minor ] use DN for more readable terms
 2022-06-16 09:35:45 +01:00
Guillaume Allais
cd324f9ff3 [ base ] Name convenience functions 2022-06-14 16:07:37 +01:00
Guillaume Allais
c9dbc3d743 [ new ] Show implementations for Language.Reflection 2022-06-14 16:07:37 +01:00
Guillaume Allais
381441d849 [ base ] maximum is an upper bound 2022-06-14 16:07:37 +01:00
Guillaume Allais
2060535d08 [ new ] name hints for primitive types 2022-06-14 16:07:37 +01:00
Guillaume Allais
a8fe4a778c [ base ] Show for Constants 2022-06-14 16:07:37 +01:00
Guillaume Allais
128099fd47 [ debug ] better eval logging 2022-06-09 23:09:38 +01:00
Thomas E. Hansen
268a3520f3 [ base ] Port most of List.Quantifiers to List1 
This doesn't include `Interleaving` and `Split`.
 2022-06-09 09:05:10 +02:00
Thomas E. Hansen
5da3bc7d7c [ base ] Port List.Elem to List1 2022-06-09 09:05:10 +02:00
Guillaume Allais
a6a4593aba [ fuzzysearch ] don't print holes 2022-06-08 22:44:55 +01:00
Guillaume Allais
7bd7f1da9c [ fix ] resugaring of DPair 2022-06-08 22:44:55 +01:00
Guillaume Allais
492abf7743 [ new ] better parse error for %language 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
88c18621e6
Merge pull request #2529 from idris-lang/revert-2496-trans-deps 
Revert "Transitive dependencies v2"
 2022-06-08 07:49:58 +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
Steve Dunham
a197300f77 Include "showmachinenames" in the output of :opts 2022-06-06 07:51:02 +01:00
kasiaMarek
094a9ab06d
List proofs (#2497) 
* Modified bind definition

* bind proofs and list elem proof

Co-authored-by: Katarzyna Marek <katarzynamarek@Katarzynas-MBP.lan>
 2022-06-01 13:16:17 +01:00
G. Allais
d786b5d153
[ IDE ] auto completions (#2511) 2022-06-01 10:26:47 +01:00
fetsorn
af04b00270 fix typo in interactive.rst 2022-05-31 09:36:05 +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
G. Allais
071d37197a
[ IDE ] intro command (#2502) 2022-05-27 10:54:34 +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
Denis Buzdalov
cb422443eb [ refactor ] Simplify %runElab wrapping code of %macro 2022-05-27 09:36:44 +01:00
Denis Buzdalov
a766c628e9 [ base ] Add mapping functions to Data.Vect.Quantifiers 2022-05-27 09:03:28 +01:00
Xerz
e9f562f435
[ prelude ] Add Range implementation for Char (#2505) 2022-05-27 07:57:59 +01:00