Fix some minor conflicts in the test suite.
Conflicts:
tests/issues/issue002.icry.fails
tests/issues/issue148.icry.stdout
tests/issues/issue198.icry.stdout
tests/issues/issue214.icry.stdout
tests/issues/issue290v2.icry.stdout
tests/issues/issue312.icry.fails
The major change in this patch is to add a new type of 'WordValue'
which is always used to represent finite sequences of bits. A word
value is either a packed word, or a sequence of lazy bits. The 'VSeq'
constructor, in constrast, is now never used for a finite sequence of
bits.
This avoids certain thorny problems that arise when trying to faithfully
implement the lazy semantics of Cryptol. We now do not have to commit
to a value at type '[n]' being represented as a packed word or as an
unpacked word until relatively late. This allows us to perform type-directed
eta-expansion at every recursive call before we know how words will be represented.
This patch fixes all the outstanding strictness bugs that I know of.
Unfortunately, we seem to lose some ground on performance. The new evaluator
is now about 5% slower than the old one on the AES benchmark, and quite a bit
slower on the SHA1 benchmark. Fortunately, the use if LRU caches for memoization
of sequences seems to keep heap usage to manageable levels; so programs generally
complete, even if they take a long time.
The definitions added in #299 cause a regression in Prelude typechecking
performance. Until we sort out the performance, we'll keep these
definitions in the module `Cryptol::Extras`.
We're only using this package for 7.8 compatibility, which will end when
GHC 8.0 is released soon. For now, just limit to the older version to
avoid import errors.
This is to set up improvements to the cryptol-server, and therefore
pycryptol interface.
This patch also fixes a regression in pretty-printing output caused by a
previous error in fixity of the `<>` operator
This notably adds a `MonadBaseControl` instance for the `REPL` monad so
that we can catch asynchronous exceptions in the middle of `REPL`
computations. Since this is a generalization of Haskeline's exception
support, that orphan instance for the console executable is now in terms
of this new instance.
This removes the `self-contained` flag, since it is fine for all builds
to have the baked-in prelude as a last resort. Tinkerers can still
change the prelude as long as it's in the search path.
Also removes some unnecessary extra prelude loading by the Cryptol
server by means of a new command
The benchmark suite no longer uses the `iteSolver` option.
Added a dependency on `deepseq-generics` so that the `NFData` instances
work correctly in Stackage LTS 2. Versions of `deepseq` before 1.4 have
a default instance that amounts to WHNF rather than NF, so benchmarks
were being measured incorrectly.
Attempt to normalize equality constraints involving a single unification
variable into a form where that variable is alone on one side of the equation.
Applying this normalization before attempting to simplify goals seems to clean
up some cases that the solver wasn't able to deal with.
