Commit Graph

2560 Commits

Author SHA1 Message Date
CodingCellist
0dbdcd30be
[ doc ] Document the System module and its submodules. (#2069) 2021-10-29 17:58:29 +01:00
Guillaume ALLAIS
d74c5f362a [ ci ] turn bootstrap-racket off 2021-10-29 17:57:55 +01:00
Guillaume ALLAIS
a8d5e005e1 [ fix #2070 ] Look under MaybeMispelling when failing quickly 2021-10-29 17:57:55 +01:00
G. Allais
96c44abb64
[ new ] :doc for keywords (#2028)
* [ new ] :doc for keywords

* [ doc ] for visibility

* [ more ] fixing help text, sentence for "mutual"

* [ doc ] for if then else

* [ doc ] for implicit arguments

* [ doc ] import

* [ cleanup ] doc for data

* [ doc ] for record

* [ doc ] for forall quantifier

* [ doc ] for `in' keyword

* [ doc ] for parameters block

* [ fix ] missing fence

* [ doc ] for where and mutual blocks

* [ doc ] for namespace blocks

* [ doc ] for with/proof

* [ doc ] for do blocks

* [ doc ] for rewrite

* [ doc ] for let binding

* [ doc ] for case...of and interfaces

* [ doc ] for fixity
2021-10-26 18:58:06 +01:00
G. Allais
ac7a4644b8
[ fix #2046 ] only refold positive integers as nats (#2064) 2021-10-26 17:16:31 +01:00
CodingCellist
20fe83de9a
[ doc ] Completely document the Data.List module (#2061) 2021-10-26 17:16:06 +01:00
Ellis Kesterton
9c2ce646f9
[ fix #2002 ] implicits used in record update (#2007) 2021-10-26 17:15:29 +01:00
CodingCellist
4a1bb310a7
[ fix #1175 ] case-splitting for inline case blocks (#2010) 2021-10-26 15:51:52 +01:00
Alissa Tung
1bd81dfbbb
[ fix #2053 ] do not show ambiguous private names (#2056)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-26 15:51:34 +01:00
G. Allais
b9834978cb
[ re #2041 ] better runtime error for holey expression (#2045) 2021-10-26 12:43:39 +01:00
Denis Buzdalov
377ae22eac [ elab ] Implement Alternative for Elab using recently added Try 2021-10-25 16:16:51 +01:00
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