Commit Graph

347 Commits

Author SHA1 Message Date
Alex Gryzlov
fb832cb49c allow empty modules 2019-07-28 12:43:25 +03:00
Edwin Brady
0bb9a13d37 Update method names when checking default methods
Fixes #42. If we don't do this, the name is treated in the saem way as
an unbound implicit, which is not what we want, so update with the
method applied to the parameters.
2019-07-27 17:01:02 +01:00
Edwin Brady
19a079511d
Merge pull request #51 from clayrat/record-fix
fix implicit/brace block ambiguity in records
2019-07-27 13:58:13 +01:00
Edwin Brady
81fefed3f3 No need to decorate implicit record fields 2019-07-27 13:19:49 +01:00
Edwin Brady
cd20ebe1af Merge branch 'abailly-check_version' 2019-07-27 12:40:19 +01:00
Edwin Brady
1a4be09f23 Merge branch 'check_version' of https://github.com/abailly/Idris2 into abailly-check_version 2019-07-27 12:31:23 +01:00
Edwin Brady
9a38d4a36d Merge branch 'clayrat-data-list' 2019-07-27 12:10:08 +01:00
Edwin Brady
0e8f10d151 Merge branch 'data-list' of https://github.com/clayrat/Idris2 into clayrat-data-list 2019-07-27 12:09:20 +01:00
Edwin Brady
5f385527c6 Remove unnecessary source file 2019-07-27 12:05:32 +01:00
Alex Gryzlov
20c57eafc1 fix implicit/brace block ambiguity in records 2019-07-27 02:16:35 +03:00
Edwin Brady
f6fa192779 Add test for fix for #49 2019-07-26 23:13:11 +01:00
Edwin Brady
f86ba8cc9b Use any local at multiplicity 0
When searching for an auto implicit, if we're at multiplicity 0 we can
use any local (e.g. when searching in a type).

Fixes #49
2019-07-26 23:10:41 +01:00
Arnaud Bailly
eb760fe20c
fix correct version to 1.3.2 2019-07-26 20:10:22 +02:00
Edwin Brady
fa76f2a78b Bind auto implicit arg names in LHS
We were only doing implicits, so add auto implicits too. It's slightly
tricky, because we might also have implicits given of the form @{x}
which stands for the next auto implicit.

Fixes #50
2019-07-26 16:58:02 +01:00
Arnaud Bailly
cb6ce92cbb
use regexp to validate idris version 2019-07-26 16:44:27 +02:00
Edwin Brady
8e9655dd9b Unbound implicits are invertible in terms
Just like all other pi-bound things, if m is an unbound implicit and we
have m ?x = m y as a unification problem, we can conclude ?x = y because
it has to be true for all ms.

This was implemented in Blodwen but I hadn't got around to it yet for
Idris2... fortunately it's a bit easier in Idris2!

Fixes #44
2019-07-26 12:27:54 +01:00
Arnaud Bailly
6c1c865587
check idris version before building 2019-07-26 09:52:45 +02:00
Edwin Brady
4f4d4ccbe9 Store invertibility in definition, not hole
This will be useful shortly, and in general because it'll give us more
flexibility in unification to be able to spot things which are
guaranteed invertible like constructors.
2019-07-26 00:00:03 +01:00
Alex Gryzlov
c3191f7d90 export decEq implementation 2019-07-24 17:13:47 +03:00
Alex Gryzlov
d289a0da4c fix names 2019-07-24 16:23:18 +03:00
Alex Gryzlov
b9b41dea40 port Data.List 2019-07-24 16:11:27 +03:00
Edwin Brady
e9f17c0afe
Merge pull request #35 from Theodus/ci
Add CI
2019-07-24 12:31:29 +01:00
Theo Butler
6ab41086a7 Add Travis CI config 2019-07-23 21:49:24 +02:00
Edwin Brady
36b5081a4e
Merge pull request #16 from clayrat/clean-ipkg
Add --clean option for ipkg
2019-07-23 15:14:02 +01:00
Edwin Brady
74e383f0c4
Merge pull request #40 from ska80/fix-missing-quotes
Add missing double quotes
2019-07-23 14:52:00 +01:00
Kamil Shakirov
71e34596cb Add missing double quotes 2019-07-23 14:54:58 +06:00
Edwin Brady
048c10a64a Update issue templates
Add "installation problem", and while I'd rather not have larger proposals on the tracker, it would still be useful to list small requests where it's objectively clear what the resolution is.
2019-07-23 09:43:18 +01:00
Edwin Brady
86eb475413 Check for name clashes in impl constraints
We were only checking parameters, meaning that there were potential
clashes leading to confusing behaviour, and meaning that it was somehow
relevant what the names were in the interface!
2019-07-22 23:16:51 +01:00
Edwin Brady
7e67ba4f35 Allow marking interface methods multiplicities
Now by marking a method as multiplicity 0, we can explicitly say that
it's compile time only, so we can use it to compute types based on other
erased things - see tests/idris2/interface008 for a small example.

This fixes #8 - at least in that it allows the interface to be expressed
properly now, although the multiplicity annotations mean that
unfortunately it can't be compatible with Idris 1.
2019-07-22 16:21:33 +01:00
Edwin Brady
9813b39be6 Update INSTALL/README
These now say Idris 1.3.2 is required
2019-07-22 16:15:51 +01:00
Edwin Brady
91262b4800 Fix possible loop in auto implicit search
A local variable can't be applied to itself when searching (otherwise,
for example, we could end up trying something like id id id id id id etc
forever). So remove it from the environment before searching for its
arguments.

This and the previous patch fix #24. (Or, at least, the minimised cases
reported as part of it!)
2019-07-22 11:21:34 +01:00
Edwin Brady
0e4c610f56 Fix for interfaces with parents
Don't use the interface itself when checking parent implementations
exist, otherwise we'll end up in a cycle (because the parent
implementation will sort of exist as a result!)
2019-07-22 11:21:34 +01:00
Edwin Brady
6a0c77257e Update issue templates 2019-07-21 14:55:40 +01:00
Edwin Brady
7f742caf3b Add icons/logos 2019-07-21 14:47:11 +01:00
Edwin Brady
e0757be43c Add template for readthedocs 2019-07-21 14:45:12 +01:00
Edwin Brady
d9719f53a5
Merge pull request #38 from chrrasmussen/docs-for-exp-log
Document base for exp and log functions
2019-07-21 13:43:33 +01:00
Edwin Brady
45b6d5165c
Merge pull request #33 from simonchatts/master
Use ahead-of-time compilation with Chez
2019-07-21 13:43:04 +01:00
Edwin Brady
256b800cab
Merge pull request #37 from chrrasmussen/fix-acos
Fix primitive function for acos
2019-07-21 13:39:31 +01:00
Christian Rasmussen
7310776603 Document base for exp and log functions 2019-07-21 02:14:48 +02:00
Christian Rasmussen
cafae8f11d Fix primitive function for acos 2019-07-21 01:47:47 +02:00
Edwin Brady
6d90b72fe9 Check under data constructor for holes
We can't begin a search until we know what we're searching for! For some
reason I forgot to add this case, and without it the search space can
explode, or we might find an answer too soon and commit to the wrong
thing!

Fixes #36
2019-07-20 21:09:33 +01:00
Edwin Brady
0b1d6527c8 Add test for #25 2019-07-20 19:01:34 +01:00
Edwin Brady
cae9162fcf Check under 'as' patterns for case arg usage 2019-07-20 18:57:03 +01:00
Edwin Brady
6dd18d798a Allow annotating functions with multiplicity
This means we can write truly type level only functions, by annotating
them with a 0 before the type declaration.
2019-07-20 18:04:18 +01:00
Edwin Brady
607e280895 Place implicits through to method bodies
This means that even if the relevant parameters aren't used by a method
body, the method can still see what the implicits are (though they will
be 0 multiplicity).

This is relevant to #8, but doesn't really fix it because we still need
a way of saying that methods are 0 multiplicity.
2019-07-20 16:25:40 +01:00
Edwin Brady
e902340346 Change elaboration of parent constraints
We need to turn pairs into separate constraints, which is a bit of a
hack but the constraints need to be separate in order to build the
chasing functions which find the parent constraints correctly.

Possibly there is a neater way, which is to teach the search algorithm
to look in the hints for pairs, but that's a lot more complicated (and
probably unnecessarily so).

Fixes #25
2019-07-19 11:51:40 +01:00
Simon Chatterjee
3bee97c0b9 Use ahead-of-time compilation with Chez
This is a bit rough, but does yield an executable with a ~40% speedup in
startup latency on one test. The resulting executable is a .so file with a #!
invocation of the local chez scheme executable to run it, so the binary isn't
portable (even to a machine with the same architecture/OS) unless there's an
identical chez installation on both machines.

As with the .ss source, the .so is currently leaked in the temporary directory.
2019-07-19 10:27:15 +01:00
Edwin Brady
677ddea9c5 Only check determining arguments at the top level
They're just about deciding whether it's okay to start an auto implicit
search, not whether it's okay to continue search, which is part of the
problem in #25.
2019-07-18 20:32:03 +01:00
Edwin Brady
f35124e76a Add note to CONTRIBUTING.md
%default directives not yet implemented
2019-07-18 20:32:03 +01:00
Edwin Brady
623024d179
Merge pull request #28 from jfdm/add-either
Inclusion of Either within Base.
2019-07-18 20:31:51 +01:00