Commit Graph

2434 Commits

Author SHA1 Message Date
Zoe Stafford
1669fc351b
Refactor %builtin (#1803)
* Stub for future 'identity' optimisation
I plan to add this later, but I'm using for now for
NaturalToInteger and IntegerToNatural

* Refactor `%builtin`
fixes #1799

- automatically optimise all Natural shaped things
- NaturalToInteger and IntegerToNatural now use
  new `Identity` flag (internal use only for now)
  which signals the function is identity at runtime

* Use NaturalToInteger and IntegerToNatural for Nat and Fin
Also define show fin in terms of finToInteger, for speed

* Fix name handling for %builtin

* [ tests ] fixes + #1799

* remove %builtin from libs
Add back after next version

* Use resolved names where convenient
2021-08-03 14:19:17 +01:00
Mathew Polzin
ed0c8d60bc
Merge pull request #1807 from mattpolzin/correct-gmp-install-directions 2021-07-31 12:56:42 -07:00
Mathew Polzin
52cc1554e3 get a bit more specific about the GMP library requirement. 2021-07-30 23:10:59 -07:00
Mathew Polzin
fe306f8e4b support explicitly setting a version tag during build. 2021-07-30 21:51:59 -07:00
Guillaume ALLAIS
94811ba8e7 [ ci ] bring racket builds back
A new environment seems to have solved our issue.
Cf. actions/virtual-environments#3774
2021-07-30 16:18:58 +01:00
Zoe Stafford
8e1ca0eddf
Add break in each case alt in js backend (#1796)
* Add `break` in each case alt in js backend
Fixes #1795

* Remove some uneeded `break`s

* linter

* Follow @stefan-hoeck 's advice
This is neater
Note: I renamed breakAfterAssignment because it's too much work to type

* [ test ] Test for #1795

* cleanup: remove unneeded vcat
2021-07-30 07:16:23 +01:00
Sventimir
4920601fe9
Add tests for Nat ranges and fix bad range [1,2..1] behaviour. (#1794)
Co-authored-by: Marcin Pastudzki <marcin.pastudzki@gmail.com>
2021-07-28 06:52:59 +01:00
Guillaume ALLAIS
84b064330c [ ci ] add collie & frex
[ci: libs]
2021-07-27 13:58:41 +01:00
Guillaume ALLAIS
c48fe486fa [ cleanup ] on is meant to be used with 2 arguments
The previous definition means it won't reduce until it's applied to
4 arguments which may have detrimental effects: ``f `on` fst`` would
for instance stay blocked, with some implicit arguments of the form
`DPair a b`. This means that `b` appears in a negative position in
the expression which may lead to positivity checking rejecting a
datatype defined using `on`!

I have decided to leave `g` and `f` on the LHS because I expect `on`
to be used either:
  1. partially applied to two arguments
  2. in a section if only applied to 1 and sections get eta-expanded
     by the parser so that's fine.
2021-07-27 13:58:41 +01:00
Guillaume ALLAIS
31ffb4e5c7 [ cleanup ] various public export & cleanup
Turns out that `Smaller` and `LT` won't unify because
1. the instance Sized Nat is not publicly exported
2. Smaller, and LT are stuck until fully applied

The given changes make that go away.
2021-07-27 09:06:20 +01:00
Mathew Polzin
b03395debe
Merge pull request #1603 from ska80/remove-realpath-notes
Remove all mentions of `realpath` from docs
2021-07-26 12:38:39 -07:00
Kamiλ Shakirov
0d03064663
Include GMP in the requirement list 2021-07-27 00:25:57 +06:00
Guillaume ALLAIS
13ef8ba707 [ fix #1782 ] remove the case-specific code
I can't make sense of this code, it seems to try to convert the
case function corresponding to `let (a, b) = f n in ...` into a
different case function where `f n` and `(a, b)` have been unified.
But if `f n` is a bona fide stuck computation, there's no chance of
this happening.

Just turning this off solves the #1782 and only breaks one function
in the whole of the idris2 repo (I would have expected our current
termination oracle to be too weak to detect it as valid anyway!)
and one in frex (which, again, should not have been seen as terminating).

Also fixes #1460
2021-07-26 17:03:16 +01:00
Guillaume ALLAIS
207a60479c [ re #1782 ] A bit more debugging info
Also making sure that the case block has the same totality as its
parent function. That does not seem to fix the bug though.
2021-07-26 17:03:16 +01:00
André Videla
aa77b7f33e
Merge pull request #1769 from andrevidela/fix-fromString-interpolation
Remove `fromString` calls from interpolated strings
2021-07-25 17:18:20 +00:00
Edwin Brady
b76050d670 Remove __collect_safe
This is to make the bootstrap build with earlier versions of Chez - we
don't strictly need it because we don't use threads (yet) and some linux
distros only have Chez 9.5.
2021-07-25 15:03:25 +01:00
Edwin Brady
c28b257fb5 Add ability to manipulate scheme objects
This is step 0 in a plan to use the scheme evaluator to evaluate Idris
expressions at compile time. As a proof of concept, I've got this
working for a toy language here: https://github.com/edwinb/SchemeEval

We won't be able to do anything interesting with this in Idris itself
until the next release because it involves updating the bootstrap code
and adding the ability to pass 'Integer' to foreign calls, which really
should have been allowed anyway since it's for a backend to decide what
it can cope with, not Idris itself.
2021-07-25 14:55:40 +01:00
Zoe Stafford
328617d6fa
Merge pull request #1781 from stefan-hoeck/file_comp
[ fix ] bash TAB completion for files
2021-07-25 08:35:43 +01:00
stefan-hoeck
a693138cc5 [ fix ] bash TAB completion for files 2021-07-24 04:48:01 +00:00
Niklas Larsson
51f59b9530
Merge pull request #1779 from melted/doc_fix
Update windows docs with gotchas
2021-07-23 16:10:26 +02:00
Niklas Larsson
4b0edbaa4f Update windows docs with gotchas 2021-07-23 15:48:54 +02:00
Guillaume ALLAIS
d0c0698c45 [ re #1771 ] Check parameters for positive uses
It's fine to allow positive occurences in (strictly positive)
parameters but we do need to check that these occurences are
strictly positive!
2021-07-23 13:30:24 +01:00
Guillaume ALLAIS
b24a9a51df [ re #1771 ] Fix another Erased-related issue (in nameIn) 2021-07-23 13:30:24 +01:00
Guillaume ALLAIS
230f42b697 [ re #1771 ] Do not use Erased to go under binders
In the `MkFix : f (Fix f) -> Fix f` example, using `Erased` for `f`
makes the type reduce to `[__] (Fix [__]) -> Fix [__]` and because
`[__] e1 ... en` computes to `[__]`, we end up with `[__] -> Fix [__]`
which does not reference `Fix` anymore.
2021-07-23 13:30:24 +01:00
Guillaume ALLAIS
df43045054 [ debug ] add a lot of logging throughout positivity checking 2021-07-23 13:30:24 +01:00
Niklas Larsson
603c60efec Add some docs about building on Windows 2021-07-23 10:58:38 +01:00
Ellis Kesterton
e5879dc687 Document --init
Reference the --init option for creating package files in the tutorial documentation.
2021-07-22 19:15:33 +01:00
André Videla
f4e1346a81 Remove fromString calls from interpolated strings
This fixes a bug where an interpolated string would
be wrapped in a `fromString` call
2021-07-22 17:13:44 +00:00
André Videla
5389f8c2a8
Merge pull request #1770 from andrevidela/fix-if-then-else-interpolation
Fix #1767
2021-07-22 16:35:11 +00:00
André Videla
6811c338cb Fix printing functions for string starter token
Co-authored-by: Andy Lok <andylokandy@hotmail.com>
2021-07-22 13:55:24 +00:00
Mathew Polzin
523c0a6d78 actually, with the change to the super linter, there's really no point in having CI work on both master and main at the same time, we just need to rename the branch right away for a smooth transition. 2021-07-22 13:42:45 +01:00
Mathew Polzin
7c85971698 Make sure main branch is covered in addition to master during the transition. Make the default branch for linting the main branch. 2021-07-22 13:42:45 +01:00
Edwin Brady
52c21c6182 Update bootstrap code
We shouldn't strictly need this, but it doesn't do any harm, and it also
means we can use --inc chez in the build if we do. Let's see if it helps
or hinders the CI problem...
2021-07-22 13:36:17 +01:00
Edwin Brady
e633a9fa6e Correct error018 test
I expect I got my local versions inconsistent while working on this...
2021-07-22 13:36:03 +01:00
Edwin Brady
edefd543f7 A bit of refactoring of argument elaboration order
In theory argument elaboration order doesn't matter, but in practice we
sometimes make choices for performance reasons, like helping with
disambiguation by knowing the target type.

This was kind of messy, now we can more clearly see what's going on.
Also, more importantly, it gives us a bit more control which we
sometimes need. For example, if we go choose to go right to left for
some performance heuristic it might turn out we don't have enough
information yet, in which case we need to delay and try again later.

Fixes #1743
2021-07-22 13:36:03 +01:00
André Videla
bab3897a9b move basic053->interpolation002, move basic061->basic053 2021-07-22 12:17:53 +00:00
André Videla
1276f47cf6 Fix #1767
The `if then else` syntax expects a block for the `then` and `else`
parts. Before this patch, the token `InterpEnd` was not a valid
follow up token to end a block. This adds `InterpEnd` as a closing
token for blocks, allowing `if then else` in interpolation slices
without additional parens.
2021-07-22 12:17:53 +00:00
G. Allais
9f0a70626a
[ ci ] turn ubuntu-bootstrap-racket off for now (#1772)
[ci: skip]
2021-07-22 12:27:34 +01:00
André Videla
5576d30c27
Merge pull request #1736 from stepancheg/test-discovery
Implement test discovery
2021-07-22 08:56:02 +00:00
G. Allais
34167d58bb
[ ci ] controlling builds via commit messages (#1766) 2021-07-21 16:49:32 +01:00
Ben Hormann
74db7714d4
[fix] Loading libidris2_support.dll with Racket (#1583) 2021-07-21 14:35:21 +01:00
Mathew Polzin
5f34801200 Make drop and drop' public exported from the vect module. 2021-07-20 14:27:43 +01:00
André Videla
ada33b90a1
Merge pull request #1756 from andrevidela/document-raw-strings
Document string literals
2021-07-19 19:38:47 +00:00
André Videla
440a3affd5
Update docs/source/reference/strings.rst
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-07-19 10:37:22 +00:00
Nick Drozd
ab36ad71cf Simplify a few Factor proofs
A few proofs have been rewritten, a few unnecessary cases cut, and
lots of unnecessary "explicit implicits" have been cut. Probably these
implicits were required when the code was initially written, and
inference has improved since then.
2021-07-19 08:30:47 +01:00
Stiopa Koltsov
eabab4bdea Split Windows CI build into multiple steps
It's easier to follow Windows CI output this way.
2021-07-19 08:02:06 +01:00
Edwin Brady
68db9fe0fe Add reg048 files
Odd, I thought I added these before, but it's probably because I got in
a mess with git and didn't re-add once I resolved that.
2021-07-19 00:21:28 +01:00
Edwin Brady
2068eb271b Better ordering of delayed elaborators
Instead of having an arbitrary looking priority number, record explicit
reasons for the delay, which helps order them sensibly when rerunning
them. Mostly this allows us to choose which ones to rerun, where it
helps, and helps order things to get better error messages.
2021-07-19 00:21:28 +01:00
André Videla
396ebe2023 Add documentation for new string literals 2021-07-18 22:32:26 +00:00
André Videla
9aa7a4303a Added documentation for new string literals 2021-07-18 21:37:20 +00:00