716 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
André Videla	cec56561c6	Merge pull request #387 from LibreCybernetics/fix-export-vect ... Make Applicative implementation of Vect n public export.	2020-07-01 17:26:08 +01:00
Edwin Brady	c4d56e5481	Merge pull request #396 from edwinb/lazy-lazy ... Don't commit to a Force too early	2020-07-01 12:29:52 +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	0d4db3ee75	Add 'force' and 'delay' as functions ... Since Force and Delay are keywords now, these may help in higher order cases in particular.	2020-07-01 11:35:27 +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
Denis Buzdalov	df60e07962	List's snoc injectivity property was renamed approporiately.	2020-06-30 13:18:42 +01:00
Edwin Brady	393c1ed464	Merge pull request #388 from edwinb/samples-dir ... Copy samples directory from Idris2-boot	2020-06-30 11:23:40 +01:00
Edwin Brady	4f10bfcfd2	Copy samples directory from Idris2-boot ... This is referred to in the documentation, so should be there	2020-06-30 10:51:09 +01:00
Fabián Heredia Montiel	e488c6cf0e	Make applicative implementation of Vect public export	2020-06-29 18:27:57 -05:00
Niklas Larsson	53621f84c5	Merge pull request #370 from ShinKage/ansi ... Adds ANSI codes support in contrib	2020-06-29 19:43:46 +02:00
Edwin Brady	a35965be84	Merge pull request #384 from edwinb/unify-invert ... Use 'unify' rather than 'convert' if possible	2020-06-29 16:22:31 +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	84477adfc9	Merge pull request #383 from edwinb/coverwhere ... Pay attention to nested names in coverage check	2020-06-29 13:52:32 +01:00
Edwin Brady	b2da2fe558	Pay attention to nested names in coverage check ... Fixes #164	2020-06-29 13:27:00 +01:00
Niklas Larsson	4db58171f9	Merge pull request #381 from chrrasmussen/avoid-traversing-modules-twice ... Avoid traversing all Idris modules twice when installing	2020-06-29 12:03:08 +02:00
Edwin Brady	31b486c8ed	Merge pull request #382 from edwinb/linear-holes ... Use precise inference for hole types	2020-06-28 23:17:59 +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
Christian Rasmussen	24bb84fcf5	Avoid traversing all Idris modules twice when installing	2020-06-28 21:36:48 +02:00
Edwin Brady	e175bb8310	Merge pull request #379 from edwinb/interface-type ... Record implicit parameters of interfaces	2020-06-28 15:31:47 +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
Niklas Larsson	cd777a00ce	Merge pull request #376 from andrevidela/kleisli-arrow ... Add Kleisli arrow operators to contrib	2020-06-28 00:18:04 +02:00
André Videla	8d04881356	Add Kleisli arrow operators to contrib	2020-06-27 22:02:05 +01:00
Edwin Brady	fb9f79e3c6	Merge pull request #375 from edwinb/interactive ... Add new clause at next blank line	2020-06-27 21:36:59 +01:00
Edwin Brady	17fec60d7a	Add new clause at next blank line ... This fixes a thing that's been annoying me in the vim mode. It's usually something that's left to the editor, but we do all the work for the vim mode! (This is hard to test conveniently, sorry...)	2020-06-27 21:09:03 +01:00
Edwin Brady	35e328a505	Merge pull request #373 from edwinb/interactive ... Various interactive editing improvements	2020-06-27 19:10:16 +01:00
Edwin Brady	929c5504c5	Implement make-case	2020-06-27 18:28:09 +01:00
Edwin Brady	c043fc3c57	Do make-with IDE command properly ... Now updates the file rather than just printing the output, in update mode. Also adds bird tracks where appropriate in literate mode.	2020-06-27 17:06:17 +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
Ohad Kammar	f31318f5e6	Merge pull request #372 from ohad/export-length-correct ... Export the `lengthCorrect` proof, as users might want to use it	2020-06-27 16:21:04 +01:00
Ohad Kammar	6683a2147f	Export the lengthCorrect proof, as users might want to use it ... Change the `len` to be irrelevant, as it's uniquely determined by matching on the input vector	2020-06-27 15:54:35 +01:00
Edwin Brady	6c007fc046	Use full names for constructors in case split ... Fixes #184	2020-06-27 15:47:38 +01:00
Ohad Kammar	574524d8de	Merge pull request #368 from ohad/fstrings ... Add a simple DYI f-string / string interpolation library	2020-06-26 21:12:13 +01:00
Giuseppe Lomurno	28018d9573	Fixed typo	2020-06-26 21:26:36 +02:00
Giuseppe Lomurno	36c62c754a	Updated documentation	2020-06-26 19:16:14 +02:00
Giuseppe Lomurno	5ccc6a397d	Added Control.ANSI module in contrib	2020-06-26 19:10:02 +02:00
Ohad Kammar	ac1fa28890	Add a simple DYI f-string / string interpolation library ... Apparently the concrete syntax is controversial ("{apples}" vs. "$oranges"), so I'm just adding a simple DYI version until we agree on a concrete syntax	2020-06-26 16:52:37 +01:00
Edwin Brady	176f2516da	Merge pull request #365 from edwinb/lineario ... Add linear network library	2020-06-25 12:58:26 +01:00
Edwin Brady	33957c4328	contrib needs to be built before network now	2020-06-25 12:12:20 +01:00
Edwin Brady	531170e949	Add linear network API ... This involves updating the bootstrap code since it needs a fix in interface resolution. It shouldn't affect the Idris2-boot build though, since it's in the libraries not the Idris2 source.	2020-06-25 12:07:33 +01:00
Edwin Brady	9576fdc1d3	LIO.run needs exporting ... It's useless without it!	2020-06-25 11:57:17 +01:00
Niklas Larsson	534fc0e073	Merge pull request #353 from stepancheg/modns ... Better TTC data is in an older format message	2020-06-25 10:47:46 +02:00
Niklas Larsson	8d75d70fac	Merge pull request #342 from csabahruska/master ... add unit test for constructor duplicate	2020-06-25 10:39:25 +02:00
Edwin Brady	0f71464ab5	Merge pull request #363 from edwinb/lineario ... More on the Linear IO experiment	2020-06-25 00:10:09 +01:00
Edwin Brady	908742c2a8	Update tests ... Seemed I hadn't cleaned thoroughly enough...	2020-06-24 23:53:42 +01:00
Edwin Brady	ebc413ede5	Postpone elaborating lambdas ... 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...	2020-06-24 23:27:45 +01:00