renderOneLine should render to one line
Previously the implementation was using layoutCompat with the hope that this operation rendered to a single line. It doesn't. This function is only used in the obscure :dumptests command where rendering to a single line is important for the file format.
Previously, `splitV` would assume that if you were splitting a value `val` into
something of type `[inf][each]`, then `val` must be a stream of type of `[inf *
each]` (i.e., of type `[inf]`). This is not true in the corner case where
`each` equals `0`, however. In that case, `val` is of type `[0]`, which is a
word, not a stream. As such, we need to ensure that we do not call `fromSeq` on
`val`, which crashes if `val` is not a stream or sequence.
Fixes#1749.
* Fix docstring behaviors around functors
- Don't duplicate docstrings onto modules generated by the desugarer
- Combine docstrings when instantiating a functor to preserve both the instance and the instantiated documentation
* Suppress :check-docstring output for definitions without fences
* Initial implementation of "check docstrings" from python
* Improve and synchronize the unlit and docstring code fence parser to better match GitHub markdown syntax
* Associate identifiers with docstring comes from
* Add :set proverTimeout support for goal-level timeouts
* Adds and evaluates docstrings on top-level module declarations
This ensures that all of the primitives defined in `lib/Float.cry` are
supported in Cryptol's reference evaluator. Moreover, this removes the
primitive table entry for `fpIsFinite`, as `fpIsFinite` is not defined as a
primitive and therefore doesn't need special treatment.
I have added a `tests/regression/float_reference_eval.icry` test case which
ensures that the reference evaluator does the expected thing on all
floating-point operations.
Fixes#1714.
Add (x >= 2, x^a * x^b = x^c => a + b = c) to Numeric.hs.
Add (Nat a, a * a^x = a^y => 1 + x = y) to SimpType.hs
Add (x >= 2, x^a >= x^b => a >= b) to Numeric.hs
Start adding tests for exponent TC checks.
* Document docstring comments in reference manual
* Handle more expected cases of prefix stripping in docstring comments
* Catch REPL exceptions when checking docstrings
* Update all commands to track their results
* Implement REPL :check-docstrings command
This command checks that all of the unlabeled and "repl" labeled
codeblocks in docstrings can successfully evaluate as REPL commands.
Cryptol will now indicate exit failure if any of REPL commands fail,
making it possible to use in automated testing.
:check-docstrings internal implementation is set up to track results
of subcommands in support for integration into a remote server API
endpoint.
* Implement :focus
* Add some :check-docstring test cases
* Update changelog
* Update CrashCourse.tex now that more commands are checked
* Require repl and convert \r\n to \n in lexer
Checking ill-typed constraint guards for exhaustivity can cause Cryptol to
panic. If we detect any type errors after type-checking the guards, we now
abort early and report any recorded errors instead of proceeding to check
exhaustivity.
Fixes#1593. Fixes#1693.
Numeric constraint guards have very particular syntactic requirements:
* They must always be used in top-level definitions.
* Their definitions must always be accompanied by a top-level type signature.
Previously, we checked these requirements in a combination of places in the
parser and the typechecker. The checks in the typechecker weren't very
thorough, however, and they failed to catch local definitions without type
signatures that use constraint guards, as seen in #1685.
This patch moves all of these syntactic checks to the parser (in
`Cryptol.Parser.ExpandPropGuards`). We now recurse into expressions to check
for local definition that use constraint guards and error if we encounter one.
This ensures that by the time we reach the typechecker, all constraint guard
expressions are at least syntactically valid.
Fixes#1685.
This synchronizes the implementation of `roundAway` in the reference evaluator
with the implementation of `Cryptol.Backend.FloatHelpers.floatToInteger`, which
expects `NearAway` rather than `Away`.
Fixes#1663.
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.
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.
