Commit Graph

1806 Commits

Author SHA1 Message Date
Edwin Brady
6d37471ccc Add --profile flag
If set, when compiling this generates an executable which generates
profiling data. Currently supported by Racket and Chez, other backends
silently ignore it.
2021-04-29 15:18:59 +01:00
Edwin Brady
3bb4333ac3 Fix whitespace error 2021-04-29 13:47:31 +01:00
Edwin Brady
c3e5689a62 Add case+lambda transformation
If all branches in a case block are a lambda, lift the lambda out. In
many cases, this can save creating a closure then evaluating it
immediately, because the function is already applied to the extra
argument.

This happens in particular with IO based code, where the extra argument
is the world token. One place where this transformation has a big effect
is 'evalRef' so the evaluator is now a bit faster (about 20% on the
small benchmark I tried it on - but no guarantees that's going to happen
on other examples!)
2021-04-29 13:44:13 +01: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
Denis Buzdalov
2287a7ff35 [ refactoring ] Some equivalent changes, mostly code styling nicened 2021-04-12 15:21:33 +01:00