While the discussion about how to refactor test framework is not
finished (#1654), make this change: move `rm -rf build` in the
beginning of the test. For these reasons:
* it is useful to inspect the contents of the `build` directory
especially after the test failure
* if build crashes mid-test (e.g. process killed), next run should
not be affected by the `build` directory from the previous run
* add `strerror` function
* move `getErrno` to `System.Errno`
* use `strerror` in `Show FileError`
* on node there's no access to `strerror`, so `strerror` just converts the number to string
Ideally we'd have a complete incremental build in CI, but that could be
a bit fiddly to set up at the moment (updating bootstrap code might make
it easier). This tests that the basic facilities work, though - there's
a lot can go wrong even in a small test like this, trust me, I have made
those mistakes :).
This involves making 'unelab' aware of nested names so that it can
remove the parameters from names in the current block. It's a bit of a
hacky solution, but it is also the easiest one.
Ideally we'd build the getter types directly, rather than using unelab,
but that's one to save for another time.
Fixes#1482
Convert `App.Control.Exception` interface to an alias to `HasErr`.
Probably `Exception` interface need to be deprecated or removed.
Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.
Fix this scenario:
```
throwBoth : Has [Exception String, Exception Int] es => App es ()
throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```
With this commit it works, before this commit it failed with:
```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).
TestException.idr:8:48--8:57
|
8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
| ^^^^^^^^^
```
Pragma once is supported by all compilers for the last ten years.
Better use it instead of include guards (which use different styles
in different files).
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
This is set to 1 second by default. Usually if it hasn't found a result
by then, it never will, but given that we find the first batch of
results then sort them, the timeout also stops us fruitlessly searching
for more solutions.
Hopefully 1s is more than enough for CI too. There is a mechanism to
change the timeout (%search_timeout) so if it turns out that CI needs
longer in some cases, we can increase it there.
I haven't documented this yet, but proof/definition search needs
documenting in general. I'll get to that.
The timer mechanism may also be useful elsewhere - I'm considering it
for ambiguity warnings, because the ambiguity depth limit isn't working
very well for that.
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing
a file is enough to get it recompiled.
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes#1510, and also now gets the error location
right as a bonus!
Because it relies on the source file that I've just fixed for the
linter. I think I've now spent more time pleasing the linter than fixing
the actual bug...
We need to fully evaluate, not just the public export names, otherwise
we don't pattern match properly and potentially generate catch all
patterns we don't mean.
Fixes#1537
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.
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.
* 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
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#1365Fixes#1277Fixes#645
- Fix off-by-one error in String reverse
- Correct order of arguments in strSubstr
- Actually use start index of strSubstr
- Reduce memory usage of strSubstr in case of overrunning string end
- Add fastPack/fastUnpack/fastConcat
- Use unsigned chars for character comparisons
- Fix generated C character encodings
We do this during desugaring because elaboration may insert valid
`?` values on the LHS (e.g. when elaborating things that cannot be
pattern-matched on and should be checked to be forced).
Where 'small' means they don't refer to other metavariables, except
right at the top level, and they don't go beyond a certain small depth,
arrived at by experimenting.
We already did a bit of this, but only for depth 0. The effect of this
is that we don't need to save out lots of metavariables, so ttc loading
is faster. This takes about 8s off the Idris build time!
We stored them as equations between terms, I think because terms are
easy to re-evaluate with new information, and because I thought we might
want to save them out. It's not usually a problem to do that. However...
Going back and forth between terms and values can be expensive if
we're stuck in the middle of a complicated unification problem, the like
of which can turn up a lot if your types are complicated. So, we need to
be able to handle this.
Now store the postponed problems as NF, rather than Term, and add a
fuction to resume evaluating a NF with an updated context.
* Banners for test pools
* Summary with the list of failing tests at the end
* Option to write the list of failing tests to a file
* Option to read the list of tests to run from a file
* Using these two latest features to add a new make target to rerun precisely the tests that failed last time
It has always bothered me that 'False' got mapped to tag 1 and 'True'
got mapped to tag 0. This doesn't change much in practice (except that
perhaps a code generator might notice some useful things in intToBool)
but I'm changing it now anyway. Also added a couple of inlinings of
boolean operations.
This saves a small amount of allocation, especially since we never
actually look at the tag in a record. We can use null? for Nothing just
like for Nil.
This also involves adding a flag to constructors and case alternatives
in CExp which say whether it's a NIL or CONS. Currently, we only do this
for Prelude.List, which already has an effect, but soon I'll extend this
to work for all list-shaped things and rather than being hard coded. We
could also imagine spotting other shapes (enumerations especially) for
code generators to spot as they see fit.
This will require code generators to be fixed to recognise the new
ConInfo flag, but you can just ignore it.
Bootstrap code also updated, because we don't currently have a way of
having separate support.ss/rkt for the bootstrap and normal builds!
This adds new `Int8`, `Int16`, `Int32` and `Int64` data types
to the compiler, thus working towards properly specified integer
types as discussed in #1048.
In addition, the following changes / corrections are made:
* Support casts from `Char`, `String`, and `Double` to all integer
types (and back). This fixes#1270.
* Make sure that all casts to limited-precision integers are properly
bounds checked (this was not the case so far for casts from `String`
and `Double` to `Int`)
* Add a thorough set of tests to make sure all bounds checks work
correctly for all supported casts and arithmetic operations
Don't just have a placeholder. While this doesn't have a huge effect (if
any) on performance, it does generate smaller output for Chez to
process, and is tidier. Perhaps it's good for other back ends too, ones
that don't optimise as much as Chez does.
Only doing named functions, not higher order functions. HOFs may be
worth doing too, if we can, since this could remove lambdas and make
fewer closures.
The increment in TTC Version is necessary because otherwise there could
be inconsistencies between libraries and clients erasure properties.
We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.
Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
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!)
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)
```
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.
This change adds logic to set up sockaddr correctly for connect and
bind, handles the AF_UNIX case for getSockAddr and expands the existing
test to cover unix sockets.
Rather than tracking how far we are from the project root in the various
Makefile commands, it's much easier to reference the build target with
with an absolute path.
On Unix-like operating systems stdio.h is usually line-buffered. As
putStr uses fputs(3) from stdio.h internally, output will be written to
standard out after a newline character is written to the buffer. Since
the prompt does not contain a newline, it will only be written to
standard output after the user presses return. I encountered this issue
on Alpine Linux which uses musl libc (instead of glibc). However, I
believe this issue is likely also reproducible with glibc. This commit
fixes this issue by flushing standard output after writing the prompt to
it. Surprisingly, `src/Idris/IDEMode/REPL.idr` already does this
correctly, `src/Idris/REPL.idr` does not though.
Given we keep getting tripped up by this, here we go:
* Namespaces
* Data names
* Record names
* Data constructor names (except for operators)
* Record constructor names (except for operators)
* Interface constructor names (except for operators)
`.proj` and `proj` are identically defined but separate functions.
This patch fixes it by defining `.proj` only once, and adding `proj = (.proj)`
for every projection.
This avoids resugaring to the wrong type when there are user defined
symbols which conflicts with builtins such as Pair.
Changed the test linear002 which was relying on this behaviour for a
user defined Unit.
Fixes#634.
We've always just used 0, which isn't correct if the function is going
to be used in a runtime pattern match. Now calculate correctly so that
we're explicit about which type level variables are used at runtime.
This might cause some programs to fail to compile, if they use functions
that calculate Pi types. The solution is to make those functions
explicitly 0 multiplicity. If that doesn't work, you may have been
accidentally trying to use compile-time only data at run time!
Fixes#1163
Now reporting an error if we can't find a package that satisfies the
constraints. The version number field can still be a string (as it used
to be) but will give a deprecation warning - and the old style version
string wasn't used anyway.
Version constraints can have an upper and/or lower bound, which can be
inclusive or not.
Add wrap on file end
use rust-style raw string syntax
use swift style syntax raw string
Update src/Parser/Support.idr
Co-authored-by: André Videla <andre.videla@gmail.com>
Escape line wrap
Resolve conflict
It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes#73 (and maybe some others).
Local hints need to reduce (just like global hints do) so we expand
their definition to the lifted name before applying them.
We're identifying the global hints by knowing that the binder name is a
nested function name. This is a bit of hack, and it'd probably be better
to record that information in the binder instead, but that's a more
substantial change than I want to do right now.
This gives us the ability to define and use implementations locally, in
where clauses/local let bindings, as well as flag local definitions as
hints.
It's not yet quite equivalent to global hints, however, since it translated
the hint to a local let binding, which doesn't reduce, so if something
relies on the reduction behaviour of the hint, it won't work. This
refinement is coming later
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
This also changes the return type of `char` and `string`. They
previously returned `()`, they now return `Char` and `String`
repectively.
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
This allows, for exmaple, to have apostrophes in module names.
Test was added only for chez, however this should be viable for all
targets with `:exec` implemented.
Things like (,) () aren't straightforward IVar's but are IAlternative's
which present options about how the term should resolve. [| |] was not
accounting for this.
broaden what Names can be reflected and refied
I did not add the Names I wasn't sure how to test but have put placeholders
that produce clearer error messages.
There's some missing flexibility in how foreign specifiers can be used with
scheme that is addressed here with minimal changes to how scheme specifiers
are read. This opens up uses for users that they otherwise would have had
to modify the compiler's support files to accomplish.
Auxiliary functions introduced in elaboration (e.g., through case splits and with clauses) now
have the same totality annotation as the function they're defined in.
Moved auxiliary function `findSetTotal` into `Context.idr` since it's
now used by `ProcessDef.idr` too.
Added a totality requirement argument to `checkClause` so that the
with-clause case could propagate it to the functions it generates in
elaboration.
Sandwhich the rhs elaboration in pattern matches with code that sets
the global, default, totality requirement to the current one, and
restores the previous default afterwards. It's a bit of a hacky way to
do it, but I don't think we have a better alternative with the current
design.
Until now namespaces were stored as (reversed) lists of strings.
It led to:
* confusing code where we work on the underlying representation of
namespaces rather than say what we mean (using `isSuffixOf` to mean
`isParentOf`)
* potentially introducing errors by not respecting the invariant cf.
bug report #616 (but also name generation in the scheme backend
although that did not lead to bugs as it was self-consistent AFAICT)
* ad-hoc code to circumvent overlapping interface implementation when
showing / pretty-printing namespaces
This PR introduces a `Namespace` newtype containing a list of strings.
Nested namespaces are still stored in reverse order but the exposed
interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
Until now namespaces were stored as (reversed) lists of strings.
It led to:
* confusing code where we work on the representation rather than say
what we mean (e.g. using `isSuffixOf` to mean `isParentOf`)
* potentially introducing errors by not respecting the invariant cf.
bug report #616 (but also name generation in the scheme backend
although that did not lead to bugs as it was self-consistent AFAICT)
* ad-hoc code to circumvent overlapping interface implementations when
showing / pretty-printing namespaces
This introduces a Namespace newtype containing non-empty lists of
strings. Nested namespaces are still stored in reverse order but the
exposed interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
All of these internal names are making the output fragile. This
cleanup should allow us to only have to update the golden file
when there is a genuinely interesting change.
- Added initial implementations for terms and values
- Error messages converted to pretty printer
- Colorization for error messages
- Color and console width option both as command line and repl command
As it was, it could break if the argument was repeated more than twice.
When checking dot patterns, we need to check that no further holes are
solved, and that the pattern variable doesn't unify with some other
pattern variable, but if it had already made progress (either for a good
or bad reason) we missed this. Fixes#536
As it was, there was significant backtracking for big expressions,
getting to the end, not finding a **, so having to try again for
application expressions. Fixes#532
This has involved quite a bit of reorganisation and some improvements in
resugaring so that the results look nice. In summary:
* Expression search now gives back a RawImp rather than a checked term,
which allows it to include case expressions
* Case with one pattern is resugared to a destructuring let
* Some name generation issues address in function generation
We look at intermediate results for local variables which are functions
that return a concrete type, or recursive calls that return a single
constructor type. In these cases, we:
* let bind the local variable/recursive call
* generate a new definition for the scope, as a 'case' function
When we recursively generate the definition, it's a bit more restricted
so as not to explode the search space. We only take the first result, we
only look one constructor deep, and we go right to left on variable
splitting so only deconstruct the name we've just added.
Sort by proportion of bound variables used, which is likely to get us
the right answer quicker. The results are generated in batches of 16 (a
completely arbitrary choice) then sorted.
This gives the number of implementations to reject before accepting one.
It's intended as a reasonably cheap way of giving multiple results from
interactive editing (e.g. the vim mode, which goes via the REPL and
--client rather than the IDE mode)
These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.
Rather than returning a complete list of results, return a pair of the
first result, and a continuation. The continuation explains how to
continue the search if the given result is deemed unacceptable (either
on encountering an error somewhere, or just if the caller wants the next
result).
This means we don't search needlessly if we're only looking for the
first result. Fixes#228
...until the definition is complete. This is necessary since sometimes
information outside the case block can help resolve interfaces, and in
the simplest case, we might just have delayed resolving a default
Integer. It turns out this was also an obscure bug waiting to happen
with coverage checking of nested case blocks (so there's a test update
there too).
Fixes#443
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.
Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.
This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
The Int represented the resolved name, but this isn't guaranteed to be
up to date after reloading and, worse, it doesn't display helpfully. I'm
bored of updating the tests which fail as a result!
This also fixes#407, which is about displaying the wrong name after
reloading the ttc.
There is an argument that, for import public, this should be automatic
(that is, the publicly imported things should be reexported with the
parent namespace). I decided not to do this, because another use of
import public which we do a lot in the Idris 2 code base is purely as a
convenience, where we still expect things to be in their original
namespace.
Also, where there's a choice between things being explicit and implicit,
I prefer to err on the side of explicit now.
So, if what you really want in an API is to reexport, you can do that,
but explicitly.
Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes#395
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes#66.
We need to make sure they are inferred again when elaborating methods,
so substitute in a _ in method types before substituting in the explicit
parameters.
In future, it might (probably will) also be useful to allow giving the
implicit parameters explicitly when defining implementations.
Fixes#374
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.
A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
We need to check below top level too, since there could be holes that
we're happy to resolve by searching. The linearity test added
illustrates a place where this is needed.
The namespace parser was not requiring a minimum indentation and instead
based its indentation on the following line, which meant that a line like:
namespace Foo
foodef : Int
placed foodef into namespace Foo instead of the module's top level.
And so made it unclear when a namespace ends.
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:
- it's easier for backend authors if the type of IO operations is
slightly less restrictive. For example, if it's in HasIO, that limits
alternative implementations, which might be awkward for some
alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
instance (I have personally never encountered one - if they turns out
to exist, again, we can revisit!)
This addresses the case where you'd see an error of:
Ambiguous elaboration at:
r <- pure []
Possible correct results:
[]
[]
[]
By changing it to:
Possible correct results:
Main.Nil
PrimIO.Nil
Prelude.Nil
The output directory was previously called the executable directory, but I changed it because the output is not always an executable (depending on the code generator).
The code generators can now distinguish between where to place the (temporary) build files and the resulting output files.
unelabBinder was losing information for the purpose of displaying names
nicely. This is typically wanted but when working with elabortation it's
useful to have all the information you can get. Things like record field
names would be lost when querying with GetType but are now retained.
It takes a long time to run, but it is basically all
the testing we need of the API, if this works it's
unlikely to be broken. It requires a change in the build
system, so don't enable it for now.
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
Without --no-index, git compares the files with their state in HEAD.
But we want to compare them to each other! This explain why we were
getting no output whatsoever.
With --word-diff=color, we can easily spot the small changes anywhere in
a line.
If a function is public export, the local definitions also need to be
public export for it to reduce properly. But if they're not, we don't
want them exported or they might affect the module hash and cause
unnecessary rebuilds.
When runing in interactive mode, the diff between expected and output is not being show,
Supposedly, Git-diff returns 0 on successful run and a non-zero for error.
However, this is not being picked up by the test suite.
We change git-diff's error reporting to be more diff like in which:
+ +ve indicates that there is a diff.
+ 0 indicates the files are the same.
+ -ve program error.
This should make diff reporting more robust.
This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.
In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...
This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
