In Chaser.hs - it appears to be breaking reloading in vim, making
interactive mode not work a lot of the time, and until someone works out
why it seems best removed...
Given that lists don't have any length invariants in their type, it
suggests that we don't care about their lengths except for totality
purposes, so these proofs merely get in the way of perfectly valid uses
of zipWith.
Resolves#2517
using stdout with node has a curious side effect. It
allocates memory that will only be reclaimed after
a new event has been scheduled. Therefore we set
a timeout every 1000 calls that will execute the
remaining code.
Added Prelude.Interactive, for the I/O things, including some
convenience functions for starting simple looping interactive programs,
which involved adding Prelude.File too, and moving getArgs to the
Prelude.
Removed a no longer relevant test.
Allow proof search on anything with constructors in the indices.
Even this isn't particularly accurate, so we really need to come up with
a proper rule, but it does lead to the expected result more often than
either trying everything, or ruling out overlapping types.
This lets the reader get the full experience of the example
and also shows the temporary file path by way of the type-checker output.
This does change the success/failure reporting text to match what I had
written, so I could copy verbatim from my terminal.
The previous success/failure messages had mismatched capitalization
(title case vs sentence case), but their verbosity might have been desirable
for a tutorial, however undesirable verbosity might be when scanning
test output.
Even though I had read the ipkg section before this, it was not clear to me
that I needed to mirror the module structure on-disk in the directory
hierarchy. Providing this info to the reader removes that chance for confusion.
When checking types of hints, don't consider the recursive call as an
overlapping constructor type, or lots of things don't get filled in
which should be.
If you had an ipkg with a sourcedir defined before using the --mkdoc option would fail saying that some source files are missing.
This is because it didn't follow the sourcedir.
If they are implicits or class arguments, it's fine for 'auto' to see
them since they're only used internally, but interactive proof search
will give odd results if it uses them. So, we make a list of names which
proof search in interactive mode is allowed to use.
Instead of guessing, it will only fill in a metavariable if all of the
available constructors/hints have disjoint types. This means you'll no
longer always get 'Nothing' for Maybe or '[]' for List, but rather
you'll get a new metavariable.
'auto' behaves as before, because the idea there is to find any old
thing with the right type.
It feels like interactive proof search should be a bit more refined,
though, because the idea of that is to find the program you really want,
rather than any old program...
More refinements to this are likely, for example refusing to fill in
with locals if there are clashing types.
