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,959 Commits 6 Branches 9 Tags 112 MiB
618c71477e
Commit Graph

1959 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Johann Rudloff
1de8b4497c HTML-Escape full documentation body 2021-04-26 22:44:03 +02:00
Johann Rudloff
3baab8abea First draft version of --mkdoc CLI switch 2021-04-26 22:44:00 +02:00
Johann Rudloff
d66bbe030a Improve LambdaLift by dropping unused variables 2021-04-26 09:57:13 +02:00
Johann Rudloff
1afece45c5 Move hand specialised foldlC into Core.Core 2021-04-26 09:55:56 +02:00
Tung Alissa
881a5e7fbc
[ fix #1328 ] print infix functions enclosed in grave accents (#1331) 2021-04-25 18:56:08 +01:00
stefan-hoeck
0858c26dcf [ refactor ] renamed value to runConst 2021-04-25 10:41:36 +01:00
stefan-hoeck
7863636490 [ new ] add Contravariant interface 2021-04-25 10:41:36 +01:00
stefan-hoeck
047fdb50dd [ new ] missing Identity implementations 2021-04-25 10:41:36 +01:00
stefan-hoeck
cb7add2eca [ new ] add Const applicative functor 2021-04-25 10:41:36 +01:00
Guardian Spirit
15bd6823d2
Add identity cast (#1332) 2021-04-25 09:22:01 +01:00
Ruslan Feizerakhmanov
70158b9dd1
REPL commands: load-package & fuzzy-search (#1318) 
REPL commands: load-package & fuzzy-search
Move REPL-related code over to its own namespace
 2021-04-25 09:13:55 +01:00
Johann Rudloff
489b85aae5 PrettyPrint: Fix SimpleDocTree.fromStream dropping parts of documents 
When flattening the `SimpleDocTree` created from a `SimpleDocStream`, the
first part of a concatenated doc was sometimes dropped, depending on the
result of the recursive call to `flatten`.
 2021-04-25 09:10:22 +01:00
André Videla
9f39ad6ba8 Implement new parameters syntax 
Previously, parameter block reused the same syntax as in Idris1:

```
parameters (v1 : t1, … , vn : tn)
```

Unfortunately this syntax presents some issues:
 - It does not allow to declare implicit parameters
 - It does not allow to specify which multiplicity to use
 - It is inconsistent with the syntax used for named arguments elsewhere
   in the language.

This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:

```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```

It also enables other features like multiple declarations of arguments
with the same type:

```
parameters (v1, v2 : Type)
```
 2021-04-23 19:02:48 +01:00
André Videla
908550c05f merge multiplicity parser 2021-04-23 19:02:48 +01:00
Ohad Kammar
9a445f57e6
[base] Minor: change the order of terms in the IntegerView (#1327) 2021-04-23 14:52:44 +01:00
Denis Buzdalov
583442b359
[ contrib ] Arithmetic on Fin (#830) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-23 12:05:13 +01:00
arty
48dc732788
[ base ] Not (a == b) implies not a == b (#1315) 2021-04-22 13:16:26 +01:00
Zoe Stafford
c75b3f7f14
Add Agda-like builtins (#1253) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-22 13:08:32 +01:00
stefan-hoeck
181b26b250 [ fix ] broken unicode parsing in JSON 2021-04-22 10:59:14 +01:00
claymager
d6583048d8
Fixes for processPackage (#1304) 2021-04-21 10:15:39 +01:00
Tung Alissa
1bf46bc458
[ REPL ] Improving :doc (fixity, totality, colours) (#1316) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-21 09:39:18 +01:00
Robert Wright
8e08e96201 Replace RefC putStrLn usages with log 2021-04-19 16:04:41 +01:00
Robert Wright
54dcace421 Rename RefC.CC file name variables 
The previous names were a holdover from when these functions were a part
of `RefC.compileExpr`. The new names more accurately reflect their usage
in this context.
 2021-04-19 16:04:41 +01:00
Robert Wright
6197351e7d Add library compilation option for RefC.CC compilation functions 2021-04-19 16:04:41 +01:00
Robert Wright
735b5bef98 Split RefC CC functions into their own file 2021-04-19 16:04:41 +01:00
Robert Wright
a538736d0c Factor RefC compilation into multiple stages 
Create functions for each of C source code generation, C object file compilation, and compilation of the final executable.
 2021-04-19 16:04:41 +01:00
Giuseppe Lomurno
581c95dc96 Minor fixes, additional docs and rebase 2021-04-19 16:02:52 +01:00
Giuseppe Lomurno
c084d285db Add some documentation about PosMap 2021-04-19 16:02:52 +01:00
Giuseppe Lomurno
a53150d90b More precise record field FCs 2021-04-19 16:02:52 +01:00
Giuseppe Lomurno
7fa6dc5f48 Added insertion to interval map and usage in TypeAt command 2021-04-19 16:02:52 +01:00
Giuseppe Lomurno
76697e7f85 New interval map data structure for FC search in metadata 2021-04-19 16:02:52 +01:00
Ohad Kammar
e130ee33f4 [doc] Minor tweaks to installation instructions 2021-04-19 14:24:06 +01:00
John Mager
fc76b5a73c Add make test to nix ci 2021-04-19 11:23:58 +01:00
John Mager
738bc4331e Update PHONY description 
- TARGET isn't phony
- distclean declared elsewhere
- Update with testenv, testenv-clean
 2021-04-19 11:23:58 +01:00
John Mager
d0db61ca35 Add testenv-clean 2021-04-19 11:23:58 +01:00
John Mager
c5d2d18568 [ clean ] Revert some from (#1240) 
Since `make test` and `make bootstrap-test` now use a different
approach, several changes no longer apply.
 2021-04-19 11:23:58 +01:00
John Mager
9b81cb19d3 Set PREFIX for tests 2021-04-19 11:23:58 +01:00
John Mager
b0242b2608 [ refactor ] Introduce NAME_VERSION variable 2021-04-19 11:23:58 +01:00
John Mager
1528583e08 [ clean ] Set PREFIX for bootstrap-test 2021-04-19 11:23:58 +01:00
Guillaume ALLAIS
96cc7fd273 [ new ] depthFirst, findFile 2021-04-19 10:58:40 +01:00
Jan de Muijnck-Hughes
0c64225521 Report time taken to check totality. 2021-04-19 10:30:36 +01:00
Guillaume ALLAIS
688e5c586c [ test ] Note that we cannot turn the whole check off 
If we were to turn the whole check off instead of just making it
(not incase || isJust (isLHS mode)) then Issue962-case would fail
because `c` would get defaulted to `Integer` and not the `Int` that
is expected.
 2021-04-16 18:12:40 +01:00
Guillaume ALLAIS
f6f2f5f5c6 [ fix #962 ] solve defaults on LHS even in case 2021-04-16 18:12:40 +01:00
Guillaume ALLAIS
9f5cacf31e [ fix ] debugging printing 2021-04-16 18:12:40 +01:00
Jan de Muijnck-Hughes
b68fa077af Added some light formatting to presentation of times for the compiler. 2021-04-16 15:11:16 +01:00
G. Allais
5946442dc2
[ new ] idris2 --init (#1299) 2021-04-15 14:08:50 +01:00
Zoe Stafford
52af4bf3c7
Add missing modules to contrib.ipkg (#1302) 2021-04-14 22:51:00 +01:00
Niklas Larsson
299a31de5b
Merge pull request #1296 from melted/windows_ci_test 
add tests to Windows CI
 2021-04-12 20:07:17 +02:00
Niklas Larsson
473b8ee740 Windows test fixes 
Translate node error codes
Strip 'b' from flags
Simplify directory wrangling in chez016
 2021-04-12 18:47:57 +02:00
Niklas Larsson
b32a2593ff Node fixes 
Don't assume that errno exists. There might never have been an error.

Quote executable path to handle path with spaces.
 2021-04-12 16:43:54 +02:00