Check for situations where a unification variable is involved in
a sum of terms not containing additional unification variables,
and replace it with a solution and an inequality.
`s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)`
Fixes#212
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.
We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.
Fixes#364
This fails on Windows and we don't really know how to fix it. The fact
that it always fails masks more interesting failures, so I think it's
better to just skip it for now.
just like any other constraint from the definition.
In particular, if the schema validity depends on an outer context,
the constraints should be solve in that outer context, not here.
Fixes#314
Recent changes resolved issue 002, so we no longer need to indicate that
it's expected to fail. Other small changes to the type checker have
made things like type variable numbers change slightly.
This change partially reverts changeset c620cbf2, which fixed#296,
which was about supporting `:t (~)` in the REPL.
As of this change, `:t (~)` will no longer work in the REPL.
The regression test for issue #296 is removed.
The new evaluator allows us to have more direct control over
evaluation order, and makes it straightforward to implement tracing
primitives. There are two new primitives 'trace' and 'traceVal' in the
Cryptol prelude that produce tracing output when evaluated.
Fixes#68
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
