Commit Graph

1092 Commits

Author SHA1 Message Date
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
Edwin Brady
854804dbfb Determining argument check below top level
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.
2020-06-24 22:07:52 +01:00
Edwin Brady
ff619951f0 Reorganise LIO to allow 'pure'
Doing this is awkward, for a number of reasons, including 'pure' not
being linear in its argument - there's no guarantee it'll be used
linearly after all - and lack of multiplicity polymorphism. Fortunately
the user doesn't have to know about the ugliness underneath!

We can look at ways to make it less horrible later :). For now, this is
starting to look like something that allows us to write linear protocols
without too much extra machinery on top of IO.
2020-06-24 21:24:15 +01:00
Edwin Brady
d8abf3b74e
Merge pull request #337 from MarcelineVQ/unelab-name
change how unelabBinder shows names
2020-06-24 17:52:57 +01:00
Edwin Brady
354830f41d
Merge pull request #359 from edwinb/lineario
Add Control.Linear.LIO
2020-06-24 00:16:44 +01:00
Edwin Brady
9ea4108c82 Also need contrib for the tests 2020-06-23 23:29:28 +01:00
Edwin Brady
8540d2fb9a Add experimental library for linear computations
In Control.Linear.LIO - allows wrapping anything that supports chaining
of linear computations (most usefully, IO).
2020-06-23 23:11:48 +01:00
Edwin Brady
f120f483a9 Default hints can use locals below top level
It's okay to use locals once we've applied the default hint itself -
it's just committing to locals too early we want to avoid. This allows
%defaulthint to be more expressive (under the assumption we want it to
be :). But shortly we will need it...)
2020-06-23 22:56:55 +01:00
Edwin Brady
a7d5a9a7fd
Merge pull request #358 from edwinb/concurrency-fix
Small concurrency fixes
2020-06-23 19:30:56 +01:00
Edwin Brady
5ed27947cb Small concurrency fixes
Conditional variables with timeout in Chez didn't work, so changed to a
consistent meaning of the timeout (microseconds). Also fix linearity of
unsafePerformIO.
2020-06-23 19:06:30 +01:00
Alex Humphreys
565ede2406 Update linear.rst
Fix typo
2020-06-22 21:23:45 +01:00
Rui Barreiro
7c7f7efe04 test node019 runs 2020-06-22 20:57:25 +01:00
Stiopa Koltsov
c140605a0f Extract Prelude.Basics, Prelude.Uninhabited from Prelude 2020-06-22 18:10:06 +01:00
Dario Vladovic
9cc1215f6c Format Homebrew install code block 2020-06-22 17:17:11 +01:00
Edwin Brady
1e6314c4cc
Merge pull request #345 from edwinb/hasio
HasIO interface for IO actions
2020-06-21 20:24:29 +01:00
TomasPuverle
833a24cb45
Updated documentation for export (#344)
Co-authored-by: Thomas Herzog <thomas-github@poto.cafe>
2020-06-21 20:17:34 +01:00
MarcelineVQ
d94b86e62c change namespace parser to have minimum indentation
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.
2020-06-21 20:17:00 +01:00
Edwin Brady
413e75b6a3 Fix documentaton error 2020-06-21 19:56:23 +01:00
Edwin Brady
0316dfa417 Remove reference to MonadIO from CHANGELOG 2020-06-21 19:41:18 +01:00
Stiopa Koltsov
ac329c337c Insert @generated marker into generated Scheme files
* `@generated` is a marked used by Phabricator to mark generated files,
  any other marker would do
* it's easier to explore source tree when it's clear which files are sources
  and which are generated
2020-06-21 19:32:49 +01:00
Edwin Brady
dbdf7dab3d Back to HasIO, remove MonadIO
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!)
2020-06-21 19:21:22 +01:00
Stiopa Koltsov
736ae1ca45 Better TTC data is in an older format message 2020-06-21 18:43:31 +01:00
Rui Barreiro
ca0c8f9d42 node018 passes 2020-06-21 17:54:50 +01:00
Edwin Brady
1b15463746 Update libraries and docs with HasIO/MonadIO 2020-06-21 15:25:40 +01:00
Edwin Brady
28855088c2 Split HasIO into HasIO and MonadIO
For things which don't require (>>=), HasIO is fine, otherwise MonadIO
gives access to the monad interface.
2020-06-21 14:46:14 +01:00
Niklas Larsson
dcf4c88e8c
Merge pull request #318 from vladimyr/homebrew
Add Homebrew installation instructions
2020-06-21 14:20:58 +02:00
Dario Vladovic
a76f4e64f5 Add VS Code settings to gitignore 2020-06-21 13:18:24 +01:00
Dario Vladovic
cc61d4d3d8
Add Homebrew installation instructions 2020-06-21 13:37:36 +02:00
MarcelineVQ
6f77c06e3e reduce sugar in confusing error messages
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
2020-06-21 11:46:08 +01:00
Niklas Larsson
06018ef6c7
Merge pull request #349 from mbaulch/fixsupport
Import fgetc and listen from libc rather than support libs
2020-06-21 11:30:57 +02:00
Matthew Baulch
916c3e7090 Import fgetc and listen from libc (where they actually reside) rather than the support libs 2020-06-21 15:24:45 +10:00
Edwin Brady
d12487f529 HasIO interface for IO actions
Also updates the Prelude and some base libraries to use HasIO rather
than using IO directly.
2020-06-21 01:18:43 +01:00
Niklas Larsson
6505be6c06
Merge pull request #341 from idris-lang/melted-patch-1
Add note about the default codegen
2020-06-21 00:35:20 +02:00
Ohad Kammar
59588a3f3a
Merge pull request #316 from ohad/fancy-preorder-reasoning
Fancy preorder reasoning
2020-06-20 22:47:25 +01:00
Csaba Hruska
6de225e4be add unit test for constructor duplicate 2020-06-20 23:39:03 +02:00
Niklas Larsson
1780bd2aba
Add note about the default codegen 2020-06-20 22:56:35 +02:00
Rui Barreiro
599789dfcd optim to ignore the value of unused lets 2020-06-20 21:41:31 +01:00
Niklas Larsson
d31e59bacf
Merge pull request #327 from chrrasmussen/add-builddir-and-output-dir
Allow overriding build and output directory
2020-06-20 20:52:33 +02:00
Niklas Larsson
0d2871db3c
Merge pull request #315 from ShinKage/repl-import-module
Module command to import module in REPL
2020-06-20 20:51:17 +02:00
Christian Rasmussen
3cbcdec4a0 Add test for builddir and outputdir fields 2020-06-20 17:24:05 +02:00
Christian Rasmussen
4fc77db2fb Silence compile message when compiling Chez programs 2020-06-20 17:23:51 +02:00
Christian Rasmussen
25f8b59c66 Fix the 'main' field in the package description
Previously it always used 'Main' as the namespace
2020-06-20 17:23:51 +02:00
Christian Rasmussen
ceb7a30c09 Update changelog 2020-06-20 17:23:51 +02:00
Christian Rasmussen
21a1245c10 Add --source-dir to CLI 2020-06-20 17:23:51 +02:00
Christian Rasmussen
67cdbd3ce4 Rename dir_prefix to prefix_dir 2020-06-20 17:23:51 +02:00
Christian Rasmussen
1f0ca85678 Allow overriding the build directory and the output directory
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.
2020-06-20 17:23:51 +02:00
Rui Barreiro
1d2f3d8883 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-06-20 15:11:08 +01:00