Previously we were just using Prelude's `readFile`, which uses the
system default locale. This meant that people writing Cryptol in other
locales might produce source files that work fine for them but not
others. Now the interpreter sets the default locale to utf8 at startup.
Additionally, the code to catch exceptions from loading modules was too
lazy, allowing exceptions to bring down the whole process when the
module contents were forced outside of the `try`.
We also assumed that any IO exception was from files not being found;
there's now an "Other IO exception" possiblity. Incorrect locales will
trigger this alternative because the actual IOException raised isn't
specific to locale errors.
There is still an issue with the encoding of finitness.
For example, if we know:
a = 1 + min b a
And we know that `b`z is finite, we SHOULD know that `a` is finite too,
but apparently we don't.
1. Preserve order of TODO list, os that we prefer unification variables
2. Stop early when looking for `x = y`.
So if we have 'a = b = c` now we'll get:
a = b
b = c
Before we would get:
a = b
a = c
Revised how we do output for `:sat` and `:prove` without arguments,
making it more clear what properties are being checked in each case.
Also reworded the output of `:check` slightly in the case where the
property has no inputs. It would be nice to make `:check` output more
consistent with the others.
Fixes a bug pointed out by @weaversa:
https://github.com/GaloisInc/cryptol/issues/127#issuecomment-64464455
In addition to the other search path changes in #127, we now will add
the directory containing files to be loaded to the search path. This
applies to:
- files loaded with a command line argument, like in the original
comment
- arguments to `:l`, so for example `:l examples/DES.cry` would work
- batch file arguments, so for example running `cryptol -b
/some/path/bar.cry` adds `/some/path` to the search path.
