Commit Graph

2028 Commits

Author SHA1 Message Date
Edwin Brady
a75887ffa6 Update error018 test output 2021-06-10 12:42:54 +01:00
Edwin Brady
18c7e2c4da Merge github.com:idris-lang/Idris2 into normalise-tweaks 2021-06-10 12:22:02 +01:00
Edwin Brady
7d235272e3 Remove redundant converstion checks in Pi types
We've already checked argument and scope types, so only need to check
mulitplicities. This saves a lot of repetition when checking lambdas.
2021-06-10 12:19:41 +01:00
Edwin Brady
a2815506a8 Remove unused 'useMetas' field
This used to be a way for checking for cycles in metavariables, but we
do a proper occurs check now so no longer needed.
2021-06-09 14:37:55 +01:00
CodingCellist
abd5432885
[ fix ] indentation of impossible clauses (#1520) 2021-06-08 17:03:06 +01:00
Robert Wright
aa94dd2351 Add RefC Char pattern matching support 2021-06-07 15:15:37 +01:00
Edwin Brady
f3a44fb240
Merge pull request #1505 from edwinb/conversion-shortcut
Add a 'shortcut' to conversion check
2021-06-05 20:02:58 +01:00
Edwin Brady
d12abbdcb5 Add a 'shortcut' to conversion check
This is an approximate check of arguments - if we can find an argument
that differs at the head, there's no point in checking further. This can
be a significant shortcut when conversion checking two large terms that
only differ very slightly, as it saves checking big arguments
unnecessarily.
2021-06-05 19:02:56 +01:00
Ruslan Feizerakhmanov
7aee7c9b7c
[ new ] --install-with-src; refactoring around FCs (#1450)
Why:

* To implement robust cross-project go-to-definition in LSP
  i.e you can jump to definition of any global name coming
  from library dependencies, as well as from the local project files.

What it does:

*  Modify `FC`s to carry `ModuleIdent` for .idr sources,
   file name for .ipkg sources or nothing for interactive runs.

*  Add `--install-with-src` to install the source code alongside
   the ttc binaries. The source is installed into the same directory
   as the corresponding ttc file. Installed sources are made read-only.

*  As we install the sources pinned to the related ttc files we gain
   the versioning of sources for free.
2021-06-05 12:53:22 +01:00
Stefan Höck
baa6051d69
[ fix ] use twos complement truncation for signed ints (#1471) 2021-06-04 10:35:07 +01:00
Edwin Brady
48f3825266
Merge pull request #1501 from edwinb/hash-fix
Read import hashes correctly
2021-06-03 23:13:10 +01:00
Edwin Brady
5fa272b8bf Read import hashes correctly
Need to use the 8 byte version of Ints for the shortcut version of
reading TTCs too, otherwise we'll read the wrong hash and build things
unnecessarily.
2021-06-03 21:57:10 +01:00
G. Allais
9e7625e613
[ log ] more readable output for elab.ambiguous (#1500) 2021-06-03 18:19:08 +01:00
Johann Rudloff
18e15e2261 [ fix ] Cast CLOCKS_PER_SEC to float before division
The cast to float needs to happen before the division, otherwise integer
division will be performed, and as a result `CLOCKS_PER_NSEC` will
always be 0 if `CLOCKS_PER_SEC` < `NSEC_PER_SEC`.
2021-06-03 17:36:11 +01:00
Denis Buzdalov
2a4197e909
[ doc ] Some documentation on := syntax of let bindings (#1487)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-03 16:49:31 +01:00
Edwin Brady
5aba3b475a
Merge pull request #1499 from edwinb/ambig-lambda
Small pruning fix
2021-06-03 16:48:54 +01:00
Edwin Brady
4a193b3cfd Small pruning fix
Check for lambdas when checking if a type might fit for an ambiguous
name.
2021-06-03 16:10:35 +01:00
G. Allais
c5b10f0b52
[ doc ] for the linear pair constructor (#1492)
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2021-06-03 13:04:56 +01:00
madman-bob
98d67499db
RefC Integer Support (#1480)
* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support
2021-06-03 10:44:42 +01:00
Stefan Höck
eccce3b7b1
[ fix ] Memoize intermediary results in JS backends (#1494) 2021-06-03 10:20:07 +01:00
Denis Buzdalov
29cc1f4248 [ refactor ] Use f <$> ... instead of pure f <*> ... in traverses 2021-06-01 20:28:49 +01:00
Zoe Stafford
24f7c9d5be
Add foldMap to Foldable (#1483) 2021-06-01 15:05:04 +01:00
Andor Penzes
6b07113762 [ feature ] Expose 'resolvedAs' and 'getSimilarNames'
For LSP these functionality is helpful. When we have a way to
request all the names we known about, we can use the information
for different purposes, such as, suggesting names to fill the
holes, or creating document symbols map for a module.
2021-05-31 11:39:56 +01:00
Guillaume ALLAIS
6df80ffee9 [ cleanup ] tests/Main.idr import list 2021-05-29 11:19:42 +01:00
Fabián Heredia Montiel
da4ee92530 [ cleanup ] Remove unnecessary Libraries.Utils.Either 2021-05-29 09:30:04 +01:00
Guillaume ALLAIS
6f839240c5 [ warn ] holes are not shadowed by implicits 2021-05-27 17:18:09 +01:00
Zoe Stafford
eb044fcf7c Support prim__codegen on javascript 2021-05-27 12:58:13 +01:00
G. Allais
d69e35cb0c
[ re #1466 ] Actually error out with -Werror (#1474) 2021-05-27 11:57:39 +01:00
Kamil Shakirov
2e61779878 [ docs ] Build docs for the 'test' package 2021-05-27 11:12:44 +01:00
Fabián Heredia Montiel
30c178c815
[ feature ] Implement -Werror (WarningsAsErrors) (#1466)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-05-27 09:23:20 +01:00
Guillaume ALLAIS
b5cbf9274d [ test ] cosmetic improvements
Put the dependency checks in the banner, e.g.:

------------------------------------------------------------------------
Base library
✓ Found Chez at /usr/bin/chezscheme9.5
✓ Found node at /usr/bin/node
------------------------------------------------------------------------
2021-05-26 19:50:50 +01:00
Edwin Brady
1329e69b5d
Merge pull request #1469 from edwinb/issue1365
Cache intermediate results in totality checking
2021-05-26 16:29:57 +01:00
Edwin Brady
a9b754e9fa Remove whitespace again
Didn't I just do this? Grr.
2021-05-26 15:54:57 +01:00
Edwin Brady
9cce0e1340 Remove whitespace in test file 2021-05-26 15:52:21 +01:00
Edwin Brady
68f6f4dbd5 Cache intermediate results in totality checking
This saves a lot of unnecessary exploring of size change graphs, which
can get over the top quite quickly if there's complex mutual
definitions, or even just a single function with an interesting variety
of recursive calls.

Fixes #1365
Fixes #1277
Fixes #645
2021-05-26 15:48:09 +01:00
Jan de Muijnck-Hughes
692054516e
A rough dump of how to debug idris2's workings. (#1464) 2021-05-26 10:19:40 +01:00
Ben Hormann
1aefab3af0 [ fix ] nproc missing for non-GNU systems 2021-05-26 09:05:13 +01:00
G. Allais
4b0f171d7d
[ help ] display logging topics and accompanying blurbs (if any) (#1467) 2021-05-26 08:16:33 +01:00
G. Allais
1fd5ccf080
[ fix #1453 ] rename cast -> coerce (#1468) 2021-05-26 08:12:58 +01:00
Fabián Heredia Montiel
f1085b98a5 [ test #18 ] Add passing tests from issue to avoid regressions 2021-05-25 23:07:59 +01:00
Fabián Heredia Montiel
704a2525f1 [ fix #55 ] Propagate linear context from Definition to Clauses 2021-05-25 19:27:02 +01:00
Fabián Heredia Montiel
d9318a260a [ Fixup #1437 ] Correct cases in cftySpec 2021-05-25 16:46:10 +01:00
Mathew Polzin
a0a417240e
Simple signal handling (#1458) 2021-05-25 16:45:46 +01:00
Stefan Höck
961683ab81
[ FFI ] Support new IntX types in foreign function types (#1437) 2021-05-25 13:57:25 +01:00
stefan-hoeck
6f90e5d2e2 [ test ] node test for System.getArgs 2021-05-25 13:26:42 +01:00
stefan-hoeck
e293d82577 [ fix ] System.getArgs on node backend 2021-05-25 13:26:42 +01:00
Kamiλ Shakirov
ad656a8d47
Remove realpath (#1457) 2021-05-25 11:01:28 +01:00
Ohad Kammar
699de70301
[contrib] More properties of vectors (#1449) 2021-05-24 08:48:00 +01:00
archlinuxxx
7ca526ee05 fix typo 2021-05-24 08:42:49 +01:00
Ben Hormann
b457d15701 [ fix #221 ] realpath alternative for macOS
Zsh is available by default on macOS
readlink -f is commonly supported on Linux and BSD
2021-05-21 18:23:50 +01:00