| Age | Commit message (Collapse) | Author |
|---|
|
New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:
time sail -no_effects prelude.sail aarch64_no_vector.sail
real 0m4.391s
user 0m0.856s
sys 0m0.464s
After running with -memo_z3 once, running again gives:
time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail
real 0m0.457s
user 0m0.448s
sys 0m0.008s
Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.
|
|
|
|
- Modified how sail type error messages are displayed. The
typechecker, rather than immediately outputing a string has a
datatype for error types, which are the pretty-printed using a
PPrint pretty-printer. Needs more work for all the error messages.
- Error messages now attempt to highlight the part of the file where
the error occurred, by printing the line the error is on and
highlighting where the error message is in red. Again, this needs to
be made more robust, especially when the error messages span
multiple lines.
Other things
- Improved new parser and lexer. Made the lexer & parser handling of
colons simpler and more intuitive.
- Added some more typechecking test cases
|
|
Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly
|
|
|
|
constraints, breaking power.
Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
|
|
|
|
constraints. Clean up Lem output a little for readability while debugging.
|
|
homs for terms that only need locations and not full annotations
|
|
|
|
This reverts commit b0efdb7172e65707cceab0eff469584217b8b589.
|
|
|
|
|
