This excludes the new SuiteB tests, and moves the `allexamples`
test into a separate directory that is also excluded. The
standard `test` command still runs all tests.
These were previously missed because the final wildcard case
kept GHC from issuing a warning. This removes the wildcard case
and issues more explict panics regarding type mismatches in the
various cases.
Fixes#850
More precisely, in both cases we unload all modules and then reload
everything (this is what `:l` used to do, while `:m` only reloaded
the current module). This fixes#668.
There are opportunities to be smarter here: in particular when we
reload modules, we do need to parse them so that we can find out what
their dependencies are, and if needed to reload those. However, if
none of the dependencies have changed, and we didn't change, then we
could reuse the current module. This could be quite useful for modules
that take a long time to load.
use that information to emit error messages rather than warnings.
This provides more specific messages than simply allowing the
affected type variables to remain uninstantiated and failing later.
It also causes some examples that otherwise would have ambiguous
types to fail earlier. This converts some test instances where
REPL defaulting would eventually succeed into examples that fail
outright instead. I largely think these instances are improvements.
Fix up the test suite. This mostly delays defaulting
warnings into "showing specific instance of polymorpic
type warnings", but requires actual fixes in a small number
of places. Those places were higly questionable, in my opinion.
This changes the way the special "Error" type is used. The error
message now contains only an explanation of what happened,
and the actual malformed type is the parameter of the error function,
which is always used at kind `k -> k` where `k` is the malformed kind.
This fixes (or at least improves) #768
This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names). However, for
user display purposes, records are presented in the order in which
the fields were originally stated.
In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).
Fixes#706
* Add docstrings for all prelude functions and fix minor style issues.
Fixes#771
* Update `CryptolPrims` documentation
* Minor updates to the prelude
* Update CHANGES
* Updates to the cryptol book and CryptolPrims
* Fix several additional docstrings
* Specify and document properties of signed bitvector division.
Fixes#677
* Fixup test
* typos and style
* Regenerate PDFs
