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
is safe for all inputs.
This is similiar to the `:prove` command, except that it ignores
the computed value and only checks for safety condition violations.
Because the value is ignored, a wider variety of types can be
checked with `:safe`. Instead of just `Bit`, any finite return
type is allowed.
This allows us to distinguish cases where counterexamples find inputs
that violate safety conditions from cases where inputs cause the
predicate to be false.
This teaches the typechecker about superclass information
so that, e.g., the constraint `Ring a` implies the constraint `Zero a`.
We do this by computing sets of constraints that are saturated under
the the superclass rules. These are used during inference type to
compute the minimal collection of constraints necessary to imply
all the found goals, and at solving time to discharge goals that
are implied by constraints listed in type signatures.
Fixes#738
