This largely reverts 54831eace2 and takes
a different approach. This way path names are normalized before feeding
them to the parser, rather than when comparing the module to be loaded
with the module already loaded. This works better because it takes into
account the current directory at the time when `loadModuleByPath` is
called.
Since multiple modules may import the same module, the module loading
process keeps track of whether a given module has been loaded already.
To do this, it looks up the module by name and, if found, compares the
paths of the two modules to check that they come from the same file.
However, these paths are not guaranteed to be normalized, so it can
sometimes print an error message when attempting to load the same module
from a file named in two different ways. This commit normalizes the file
paths before comparing them. Alternatively, it may make sense to enforce
an invariant throughout that module file paths are normalized, though
this may require care to avoid overly verbose messages.
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.
Previously, we would factor out constants from `min`, now we push them in.
Thus: `3 + min a b` becomes `min (3 + a) (3 + b)`.
This allows nested `min` to flow next to each other and interact.
We also add rules for moving constants out of nested `min`:
min a (min K b) ~> min K (min a b)
and another useful rule, which sort of factors out the constants again,
but notice that the result does not have a `min` in it.
min (K1 + a) (K2 + a) ~> min K1 K2 + a
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.
Make values lazier with respect to when they produce divide-by-0
errors. Divide-by-0 should now propigate in the same way that
user errors do.
In addition, fix a bug in the reference evaluator with respect to
divide-by-0 handling of pmod and pdiv. Previously, the `polyDivMod`
function would raise a division by zero error, in contravariance
to the reference implementation invariant that errors may only
occur when forcing values at type `Bit`.
Simplifying constraints of the form `k1 + a == k2 + b`. If `k1 > k2`,
then the constraint can be rewritten to `(k1 - k2) + a == b`, or
`a == (k2 - k1) + b` otherwise. This allows the constraint solver to
make progress in cases where `a` or `b` include unification variables.
Cryptol could not prove that subtracting `65 + padding` from `512 * chunks`
in the constraint `msgLen == 512 * chunks - (65 + padding)` was well
defined, and rejected the function. This constraint was redundant, so
removing it allowed the function to typecheck.
The width table in CryptolTC.z3 wasn't large enough to solve constraints
about the width of 64-bit words. This change is a bit of a band-aid, as
larger words will expose the same problem. Longer-term, we should try to
solve these constraints after the SMT-based phase, using some other
approach.
The constraints in CryptoBox were too permissive, and when adjusted to
represent the true intent (that values fit within 64-bits), and the
width table was updated, the example will type-check again.
Thanks to @tommd for tracking both of these down.
When the constraint is of the form, `k1 * x = k2 * y`, and `gcd k1 k2 /= 1`,
simplify the constraint to `(k1 / gcd k1 k2) * x = (k2 / gcd k1 k2) * y`.
(NOTE: this doesn't produce a new constraint that uses division, but
evaluates the two two constants.)
