Commit Graph

2749 Commits

Author SHA1 Message Date
Denis Buzdalov
a47b3d7d0e
[ new ] Elaboration interface (#1860) 2021-10-25 16:16:13 +01:00
Denis Buzdalov
c340e0e713 [ cleanup ] Move left autos that are most likely to be passed explicitly 2021-10-25 13:17:03 +01:00
Zoe Stafford
3717801b8a Add some docs for logging topics
Also fix some typo
Also add 1 doc comment

Some code cleanup/optimisation too:
- with vmcode interpreter, don't generate indentation
  if it's not needed
- don't add inline if function marked noinline
- remove some unused logging topics
2021-10-25 13:14:08 +01:00
Mathew Polzin
f078d5f5dc
clean up some deprecations (#2057)
* deprecate Data.Nat.Order.decideLTE

* Add properties for LTE/GTE that produce the difference.

* remove deprecated function now that it is available in the base library.

* remove two deprecated lines.

* remove module deprecated since v0.4.0

* fix prelude reference to renamed primitive.

* finish removing Data.Num.Implementations

* remove deprecated dirEntry function.

* remove deprecated fastAppend. Update CHANGELOG.

* replace fastAppend in test case

* replace fastAppend uses in compiler.

* remove new properties that weren't actually very new.
2021-10-24 12:06:57 +01:00
Giuseppe Lomurno
7f63a0103f Add user hints to expression search 2021-10-24 10:24:22 +01:00
alissa-tung
453305fb6e [base]: add appendFile 2021-10-23 15:20:22 +01:00
Gergo ERDI
e2bf39bdea Escape continue and break keywords (#2050) 2021-10-23 15:17:11 +01:00
toyboot4e
17e67e65d4 [ typo ] In INSTALL.md 2021-10-23 15:16:23 +01:00
Denis Buzdalov
58103d9d44 [ doc ] Mark code examples as Idris code in implementation overview 2021-10-21 21:40:18 +01:00
Guillaume ALLAIS
2ee06e9db0 [ fix #2034 ] Productive cantor for Colist1 2021-10-21 16:01:02 +01:00
Guillaume ALLAIS
8fde63396e [ fix #1626 ] Empty lines are still lines 2021-10-21 16:00:50 +01:00
Guillaume ALLAIS
b16a1297b6 [ cleanup ] parser for strings using SnocList 2021-10-21 16:00:50 +01:00
Daniel Kröni
aa107a9754
Implemented %noinline (#2027)
* Implemented %noinline

* Removed trailing spaces.

* Added missing case in Reify FnOpt

* Added error message when both %inline and %noinline are set.

* Added test.

* Changed from perror to error
2021-10-19 15:22:36 +01:00
Tim Engler
670f759c7d Fixed problem where dirEntries leaks directory handles. 2021-10-19 09:36:48 +01:00
Mathew Polzin
a2ea7a76f4
Improvements to System.Random, specifically JS support. (#2009) 2021-10-19 00:04:25 +01:00
Denis Buzdalov
7833829c43 [ base ] Add couple of properties of either function with mappings 2021-10-18 20:11:38 +01:00
Daniel Kröni
5e7eece1cc Make asHex take Bits64. 2021-10-18 12:20:52 +01:00
André Videla
e4d566b28c
Update documentation and changelog for string interpolation (#2013)
* Update documentation and changelog for string interpolation

* Fix typo in changelog

* fix documentation about desugaring of interpolate

* Update CHANGELOG.md

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-10-18 11:45:32 +01:00
Edwin Brady
40f72e74f0
Case building performance/heuristics (#2020)
* Case tree/coverage checking shortcuts

We were calculating some things we didn't need - we can stop computing
the type of a case operator when we know the head, because that's all we
need for coverage checking. We can also abandon checking a left hand
side for coverage purposes if we encounter an empty type. Both of these
can save quite a bit of time in complex cases.

* Normalisation heuristic for pattern variables

If they get bit, fully normalise (like we do with case types) since it's
likely a big term with lots of applications will normalise a lot.
2021-10-17 18:21:35 +01:00
Guillaume Allais
2ce4831010 [ base ] swap for these 2021-10-17 16:57:04 +01:00
Edwin Brady
75716cd0d1
Fix casts in scheme evaluator (#2011)
* Fix casts in scheme evaluator

We really need test cases for all the primitives before we can use this
evaluator properly. Also test cases that run inside an environment,
which are a bit harder to construct.

* Add the cast fixes to racket support code

* More racket compile time evaluation fixes

We had the chez version of some primtives in the ct-support file. We
need a full set of tests for the primitives here too...
2021-10-16 14:19:26 +01:00
Edwin Brady
8932bc6d79
Change default nf_metavar_threshold (#2012)
We recently changed the meaning of this (calculated during 'quote'
rather than after) and by experimentation it seemed to be too high. It
is a somewhat arbitrary heuristic to decide when to fully normalise, but
this seems to help as a better default in some cases.
2021-10-16 12:43:12 +01:00
Edwin Brady
cfb7395eac
Add try primitive to reflection library (#2008) 2021-10-16 11:24:12 +01:00
stefan-hoeck
62237f74ea [ fix ] fastConcat for JS backends 2021-10-14 14:58:51 +01:00
Guillaume ALLAIS
1877e66309 [ new ] log sugared term Elab primitive 2021-10-14 14:16:14 +01:00
G. Allais
00ab9573a5
[ re #1944 ] Allow toplevel aliases (#1952)
* [ re #1944 ] Allow simple toplevel aliases
* [ done ] toplevel aliases with arguments
* [ fix ] weird nonsensical test case
* [ fix ] golden test files
2021-10-13 21:55:23 +01:00
André Videla
274954998b
Implement generic interpolation (#1967)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-13 17:26:54 +01:00
Zoe Stafford
5c41c81883
Optimise away case statements on unit-y types (#1844) 2021-10-13 15:46:02 +01:00
DrBearhands
7a4af0cad4 FIxed typo: repeated word 2021-10-13 14:25:32 +01:00
Tim Süberkrüb
f73e79c3f3 Make --prefix respect IDRIS2_PREFIX
Fixes #737
2021-10-13 13:29:35 +01:00
Attila Lendvai
dbba5087fe [ fix ] missing idris2_popen/pclose decl in the C headers 2021-10-13 13:25:48 +01:00
Guillaume ALLAIS
a507b6dadf [ new ] better docstrings for primitives 2021-10-13 13:17:48 +01:00
Guillaume ALLAIS
d1041cf786 [ more ] Hints for primitive types too! 2021-10-13 13:17:48 +01:00
Guillaume ALLAIS
122b89d7ae [ refactor ] a bit more principled 2021-10-13 13:17:48 +01:00
Guillaume ALLAIS
7ebaa23439 [ new ] list hints attached to a data type 2021-10-13 13:17:48 +01:00
Edwin Brady
dd95a549d5
Fix performance regression #1991 (#1995)
* Normalise types fully at the REPL

It was a bit odd that we only normalised the scope of function types and
not the arguments, and I can't remember the reason for that if there
even was one.

* Better way of using nf_metavars_threshold

If a term is getting big and probably needs normalising, we now have a
sizeLimit flag in quote, so we can use that instead of checking the size
afterwards. This is a handy heuristic for speeding up unification when
there's a term with lots of suspended computation. Fixes #1991
2021-10-11 23:53:52 +01:00
Stefan Höck
1ebe204c3f
[ refactor ] use proper int types for Constant (#1964)
* [ refactor ] user proper int types for Constant

* [ cleanup ] declare standalone TTC implementations for BitsN/IntN

Rather than doing the casting inline, have the (en/de)coding all
side by side in one place

* [ cleanup ] remove duplicated code

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-08 12:07:11 +01:00
Alissa Tung
e15c78ce9e
[ fix #1970 ] error on mod self ref (#1977) 2021-10-08 10:09:17 +01:00
Zoe Stafford
d4263441b7
[ new ] Some optimisations mainly involving Nat and Fin (#1817)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-07 19:21:32 +01:00
Dr. ERDI Gergo
8b8ddfce5c Add buildExpressionParser, based on Parsec's implementation 2021-10-07 16:14:02 +01:00
Guillaume ALLAIS
0a29d06fea [ fix ] test runner 2021-10-07 16:07:03 +01:00
Guillaume ALLAIS
384c8874c2 [ fix #1979 ] use virtualised locs rather than EmptyFCs
For error reporting purposes it's better to have an (approximate)
virtual location for code that was introduced by the elaborator
than to have an `EmptyFC` that does not help.
2021-10-07 16:07:03 +01:00
Guillaume ALLAIS
e8aa95479c [ cleanup ] remove duplicated code 2021-10-07 16:07:03 +01:00
Robert Wright
937ab7157c Add Cast to JSON interface implementations 2021-10-06 18:35:25 +01:00
Robert Wright
8c44f423cc Add JSON Show as Idris code interface implementation 2021-10-06 18:35:25 +01:00
Mathew Polzin
76b90cc816
Merge pull request #1960 from attila-lendvai/fix-install-libs 2021-10-05 11:03:33 -07:00
G. Allais
7936bf77d7
[ fix #1744 ] Compare names by root rather than UserName (#1975) 2021-10-05 15:06:16 +01:00
Attila Lendvai
cab5a0a19b
makefile: propagate IDRIS2_INC_CGS=${IDRIS2_CG} to install-libs
Without this change install-libs will not install the .so files, and
consequentially the test 'chez/chez033' fails with 'Error: INTERNAL
ERROR: Missing .so:Prelude/Cast.so' when it is run by an installed
executable.

Also add a test-installed makefile target to run the tests using the
installed executable.
2021-10-04 17:43:00 +02:00
Guillaume ALLAIS
5f314bf103 [ fix idris-hackers/idris-mode#542 ] Bring Metavars back
IDEmode's `Metavariables` should not simply be a wrapper for REPL's.
2021-10-04 14:12:15 +01:00
Guillaume ALLAIS
bb5a891f26 [ refactor ] Share the duplicated code via prettyHoles 2021-10-04 14:12:15 +01:00