This only checks that a function with signature [32] -> [32] -> [32] will
succeed with the :dumptests command. More tests could/should be added.
Since this test creates a file called add32.out, I added tests/regression/*.out
to the .gitignore. I'm not sure if this is the right approach or if we should
make an attempt to clean up this subdirectory after the tests finish.
the reference implementations. The `:check` commands are really the
only ones of interest for correctness of the algorithms.
The `:prove` commands end up just checking
the reference implementation against itself, but this checks that the
primitive redirection code is working properly.
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.
This works around SBV8.7/CVC1.7 compatiblity issues, and has a side
effect of completing the QOrdCompatible proof, which was previously
returning UNKNOWN.
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
This includes a set of declarations in a file to test the rules
in the context of type checking. It also includes a set of type
queries to test the rules (or absence of rules) in the context
of type inference.
These are useful for switching between rationals and floats.
This also cleans up the implementation a bit, removing some duplicated
code.
NOTE: I am not sure if the translation from `float` to `rational`
is quite right in the what-4 backend, but I can't think of a better
way to do it at the moment.
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
Previously, "include" used locale-dependent decoding of source files,
while the rest of Cryptol uses UTF8. This change makes "include"
consistent with the rest of Cryptol, and adds a test that checks for
malformed UTF8.
This reverts commit 85bff672ef.
The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.
Fixes#673.
Fix build with GHC 8.8
Also updates CI to use GHC 8.4, 8.6, and 8.8 on both Travis and AppVeyor, and makes some small tweaks to make the tests pass in all six configurations.
Currently we only use this for the Prelude, which is baked into Cryptol.
Previously we used to save it in a temporary file, which would show
up in error messages, leading to bad user experience and unreliable
test outputs.
Also improves the shadowing errors.
Fixes#569
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
The name "demote" is only meaningful to those who already know what
the Cryptol primitive does. Also, due to recent changes in the error
and warning messages, the name "demote" is showing up much more often
in REPL output. For example:
Defaulting type argument 'rep' of 'demote' to [2]
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
These messages will hopefully be made less confusing to non-experts
if the name "demote" is replaced with "number".
Shadowing a name from the Cryptol prelude produces an unpredictable
warning message with a temporary file name, which is not good for our
regression test suite.
