This ensures that the constraints and right-hand side expressions in each guard
are well formed. This check suffices to catch the bug in
https://github.com/GaloisInc/saw-script/issues/2043, which was fixed separately
in a previous commit.
I have also updated the `tests/constraint-guards/type-sig-constraint.icry` test
to use `coreLint=on` rather than checking `debug` output, as the former is more
resilient to internal changes in Cryptol's pretty-printer.
Fixes#1647.
Previously, `checkPropGuardCase` would not consider type signature constraints
when determining how many proof applications to generate, which ultimately led
to the issues observed in https://github.com/GaloisInc/saw-script/issues/2043.
This is relatively easy to fix by ensuring that we pass these constraints as an
additional argument to `checkPropGuardCase`.
It is difficult to fully validate that this fix works without SAW, but I have
checked in a smoke test that checks if the guards in a numeric constraint guard
definition have the expected number of proof applications.
- p-1 bits in an IEEE float refers to the significand, not the
mantissa, at least according to the latest preferred terminology,
which aims to keep the word "mantissa" for the full mantissa
including the units bit;
- reciprocal rather than reciprocol;
- the example in 1.23 had the wrong module declarations; also insert a
separator word between the verbatim blocks so they can be told
apart.
Haskell Language Server still struggles a bit with opening projects that
are subprojects of larger projects (in the git submodule sense).
When opening such projects from within their parent project, the overall
project path remains the outermost one, which breaks relative paths of
subprojects.
The file-embed has a utility to help with such path adjustments.
Theoretically, HLS will eventually support "multi-home units", where
different files will be compiled under different home folders if they
belong to subprojects, but in the meantime, this un-breaks HLS for users
that open Cryptol as a subproject of, say, SAW.
We must treat built-in abstract types slightly differently from user-defined
abstract types.
Also fix a bug in the way that the return kind of primitive types are computed:
we previously said that they all return `*`, but this is not necessarily the
case.
