idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity
873 Commits 5 Branches 9 Tags 99 MiB
ccf441f42b
Commit Graph

210 Commits

Author SHA1 Message Date
Rui Barreiro
ccf441f42b fix #447 2020-07-12 10:13:45 +01:00
Matthew Ess
6452cdbbd4
Add Ord implementation for Either (#439) 2020-07-09 19:28:59 +01:00
Edwin Brady
23cbc28b1d
Merge pull request #415 from rbarreiro/javascript 
Javascript
 2020-07-08 22:27:58 +01:00
Edwin Brady
28b52fbc48
Merge pull request #432 from edwinb/docstrings 
Initial implementation of :doc and :browse
 2020-07-08 18:28:14 +01:00
Edwin Brady
6dce3a0735 Add :browse 
Lists all the names in a namespace with their types, and the first line
of their docstring if it exists
 2020-07-08 17:56:54 +01:00
Edwin Brady
b0c226f05b Extract interface info from hints 2020-07-08 17:21:28 +01:00
Edwin Brady
656a9d8f98 Also display methods of interfaces 
Displaying implementations is a better harder at the moment, since
they're implemented via search hints...
 2020-07-08 16:52:56 +01:00
Edwin Brady
ff46a8db14 Initial implementation of :doc 
It's not pretty, but at least it exists now
 2020-07-08 15:52:57 +01:00
Guillaume ALLAIS
301666b91d [ fix #423 ] --repl should load the main file 2020-07-08 15:29:37 +01:00
Edwin Brady
2959829605
Merge pull request #426 from edwinb/record-implicits 
Leave implicit record fields alone on update
 2020-07-08 00:33:23 +01:00
Edwin Brady
58359c2d01 Leave implicit record fields alone on update 
Unless an explicit update is given
 2020-07-07 22:36:15 +01:00
Matus Tejiscak
634fe4d171 Fix tests. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
a4c59204c5 Add postfix projection sections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
ca2c9163c7 Implement %language PostfixProjections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
c9aa733626 Add more test examples. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
b46064f688 Update docs and tests. 2020-07-07 21:06:35 +01:00
Rui Barreiro
2feb4b8299 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-07 14:18:00 +01:00
Nick Drozd
7d5788471d Update tests 2020-07-07 10:48:23 +01:00
Edwin Brady
77ad6eac0a
Merge pull request #422 from edwinb/record-implicits 
Pay attention to implicits in record update
 2020-07-06 18:06:43 +01:00
Edwin Brady
0cf37f621b Pay attention to implicits in record update 
Resolves #421
 2020-07-06 17:39:55 +01:00
Rui Barreiro
3acc30599e Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 17:09:11 +01:00
Niklas Larsson
468c8cbae3
Merge pull request #414 from melted/simple_parser 
Add a simple parser combinator library for strings
 2020-07-06 17:16:19 +02:00
Edwin Brady
abdadead0a More liberal with alternatives in with blocks 
Only need to match one possibility (it's essentially impossible to match
more than one after all!). Fixes #297.
 2020-07-06 14:23:15 +01:00
Edwin Brady
666ecb36b5 Preserve @ patterns when totality checking case 
Resolves #300
 2020-07-06 14:03:34 +01:00
Edwin Brady
e25f0a57f9 Use correct implicit generation function 
Should make a default implicit, not an auto implicit, when running out
of arguments and expecting a default implicit. Fixes #371
 2020-07-06 14:02:45 +01:00
Niklas Larsson
52c6db09d1 Add <?> for replacing error messages 2020-07-06 14:13:56 +02:00
Rui Barreiro
b3216758e9 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 11:32:59 +01:00
Niklas Larsson
af83c9303b Add test and documentation 2020-07-05 21:51:12 +02:00
Edwin Brady
8774df8800 Use a String, not an Int, for case/with names 
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.
 2020-07-05 20:02:50 +01:00
Rui Barreiro
35961676bc changed tests 2020-07-05 18:55:34 +01:00
Edwin Brady
5487290499
Merge pull request #282 from ether42/master 
Fix MkRecord signature
 2020-07-05 14:03:57 +01:00
Rui Barreiro
88f8e745b1 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-05 12:19:45 +01:00
Rui Barreiro
4db8c84fe3 self tail rec 2020-07-05 11:53:45 +01:00
Edwin Brady
2ce0335fd5 Implement qualified do 
This allows do blocks to be qualified with the namespace that the (>>=)
operator is defined in. Inspired by Purescript's version of the same
thing, and this ghc proposal:
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0216-qualified-do.rst
 2020-07-04 23:01:43 +01:00
Edwin Brady
45a9668370 Export all of the Prelude as Prelude 
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.
 2020-07-04 21:57:54 +01:00
Edwin Brady
028624a18d Add "import X as Y" properly 
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".
 2020-07-04 20:26:49 +01:00
Alex Gryzlov
afde930e7a
Vect updates (#335) 2020-07-04 11:02:04 +01:00
Edwin Brady
e7830b2b40 Merge github.com:idris-lang/Idris2 into lazy-lazy 2020-07-01 11:59:35 +01:00
Edwin Brady
c216e1c560 Update test output 2020-07-01 11:53:06 +01:00
Edwin Brady
669e50ff55 Remove my debugging noise from test case 2020-07-01 00:43:33 +01:00
Edwin Brady
25491060e2 Don't commit to a Force too early 
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
 2020-07-01 00:40:44 +01:00
Mark Barbone
4916dd23a9
Make Data.Vect linear (#333) 2020-06-30 15:05:19 +01:00
Edwin Brady
a52308d77d Add test files 2020-06-29 15:13:42 +01:00
Edwin Brady
ffbea6d160 Use 'unify' rather than 'convert' if possible 
'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.
 2020-06-29 15:04:32 +01:00
Edwin Brady
b2da2fe558 Pay attention to nested names in coverage check 
Fixes #164
 2020-06-29 13:27:00 +01:00
Edwin Brady
cc03a4cb3b Add missing test file 
Apparently I forgot the input for linear012. Oops!
 2020-06-28 22:28:56 +01:00
Edwin Brady
ff7d3a0246 Use precise inference for hole types 
That is, don't generalise multiplicities, because we need the hole type
to be precise wrt multiplicities. Resolves #189
 2020-06-28 22:16:15 +01:00
Edwin Brady
8ddac9c1d5 Record implicit parameters of interfaces 
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
 2020-06-28 14:58:57 +01:00
Edwin Brady
929c5504c5 Implement make-case 2020-06-27 18:28:09 +01:00
Edwin Brady
1b695bcc52 Display binder if it's not implicitly bindable 
This is particularly important if we're generating something that needs
to be parsed and checked again. Fixes #185
 2020-06-27 16:26:34 +01:00