These allow users to test equalites between type variables and
branch on the results. This could nearly be accomplished by
instead demoting the value of the numeric expressions to integers
and comparing them as integers. However, this required `fin`
constraints on the expressions, which is sometimes undesirable.
We also implement the `coerceSize` operation discussed in
issue #704. We may decide to make this a primitive at a
later time.
This required a fair amount of fixup to the pretty-printing code,
as some of the primitives have semantics that differ in subtle ways
from the old package. The output now is mostly the same as before,
although some improvements have been made here and there.
The one somewhat negative outcome of this change is that the
"line fill" algorithm in `prettyprinter` works a bit different
and makes choices about where to break lines that are arguably
less desirable than before. When laying out structures nested inside
sequences, it is more likely to break a line inside a substructure,
whereas the old algorithm prefered to break lines between elements
of the outer sequence. There are also appear to be some minor
differences regarding how ribbon width is calculated.
Previously, when indexing into a sequence, there were code paths
in both the SBV and What4 backends where an if/then/else tree
would be built to compute the value of a symbolic lookup, with one
branch for each valid sequence index. They differed, however, in
what value they would comute for out-of-bound indices. For SBV,
we would compute a `zero` value, whereas for What4 we would
raise an error. For What4, this resulted in unfortunate and redundant
proof obligations, as we elsewhere add a test for in-bounds contditions
to the safety predicate. Moreover, the strategy of returning a
`zero` value could panic in some situations, as not every type
has a `zero` value anymore (e.g., newtypes).
In both cases, we now do the same thing, which is not to have a case
of the if/then/else tree for out-of-bounds indices; the final element
of the sequence will simply be returned instead. We will only raise
an out of bounds error in this code path if the sequence is actually
empty.
Fixes#1239
* fix(rpc): reset TC solver on file/module load
Some difficult to reproduce bugs regarding the RPC server hanging
(https://github.com/GaloisInc/cryptol/issues/1250) seemed to be
related to the type checker solver (Z3) hanging after periods of
extended use. I.e., a module would load/error quickly normally,
but if preceded by enough prior solver/server activity, Z3
would consistently hang. To avoid this, we can simply reset the
solver and reload the type checker prelude when the server is asked
to load a file or module. This solves the Z3 hang issues in observed
cases and requires no additional forking (which we're trying to
minimize when possible).
The syntax looks like:
```
let f : Integer -> Bool; let f x = x == 0
```
The leading `let` is not the most beautiful, but it gets
the job done and prevents parser conflicts.
In particular, we can now define operators using `let` in the
same way that they can be inside modules and `where`.
In addition, we allow `type` and `type constraint` definitions
at the REPL, and `infix`, `infixl` and `infixr` declarations.
Becase it is an error for an infix declaration to be stated
without its corresponding declaration, we have added the ability
to enter multiple definitions at once, separated by `;`. This
is also useful for definition mutually recursive definitions using
`let`.
* Disable Windows RPC tests
They seem to hang instead of failing at the moment, so until we get them
working it seems like it's better to just leave them out.
* Attempt to make "portability" build only run nightly.
* feat(rpc): logging for server and client
* fix: CryptolConnection dflt val for proc
* fix: activate logging on connection, not process
* chore: remove unnecessary proc field
This should avoid a potential (rare) race condition where the callback
for a dead solver runs after a new solver has already been started,
which would result in a "lost" solver process just hanging around
