Added
- Introduce a generic
pp_gen pretty-printer for error messages, so that external tools can pretty-print errors in the same style #326 - Add ppx rewriter to display gospel contents as documentation with odoc #288
- Add specific error message for patterns with guard on every clause. #220
- Added
when guards in pattern-matching #206 - Added a
with construct to name a variable in type invariants referring to a value of the specified type. #218 and #187 - Added support for
int literals. #175 and #177 and #223 - Added the
Failure exception to the Stdlib. #154 - Added a
gospel dumpast command. #98 and #184
Improved
- Forbid
old operator in precondition clauses (requires and checks) #335 - Display a warning when encountering an
include #334 - Allow patterns in arguments and return type annotation in anonymous functions #309
- Propagate pattern locations to report errors to the precise patterns #308
- Support partial application of functions and enforce OCaml syntax for constructor application #290
- Add a pretty-printer for locations #294
- Gospel preprocessor does not fail when the file is an implementation file #265
- Rename standard library
Seq and 'a seq to Sequence and 'a sequence. #253 - Allow unit result in function header #215
- Highlight source locations when reporting errors. #214
- Check for pattern-matching redundancy in terms. #213
- Check for pattern-matching exhaustivity in terms. #170
- Issue a warning when a function returns
unit but has no modifies clause. #185 - Improved locations for syntax errors in specs. #164
- Documentation improvements. #108 and #110 and #149
- Added sanity checks to type invariants: invariants are only allowed on private or abstract types. #117 and #116
Stdlib changes. #102
- Removed
ref operator. - Removed
elements for Bag and Set. compare functions returns integers instead of ints.
Fixed
- Fix the performance issues in the preprocessor \353
- Gospel preprocessor support documentation for ghost declaration #331
- Consider comments as spaces while preprocessing (to ensure specification can be attached to a ghost function or type, for instance) #321
- Fix source-location tracking (directives and overridden filename) #319
- Set up location in parsing ghost specifications #310
- Check that all patterns in a disjunction bind the same variables #300
- Handle the special case of
MODULE_ALIASES in stdlib.mli in the parser #306 - Take recursivity into account when typing type declarations #304
- Support pattern with cast #301
- Use payload location for specification text #299
- Support patterns of one-parameter constructors with a tuple argument #297
- Use correct location for arity mismatches in type applications #258
- Avoid uncaught exception when displaying a warning for builtins (using
Location.none) #283 - Gospel preprocessor no longer detach documentation below a declaration #281
- Fixed pattern match analysis in exceptional postconditions #277
- Avoid uncaught exception when displaying a warning on a dummy position #262
- Constants can now be referenced in specifications. #211
- Infix operators in specificaion headers are now accepted. #205
- Fix inconsistencies in typing/parsing of exceptional postconditions patterns. #203
- Fixed the type-checking of interfaces involving the OCaml Stdlib, which was not opened by default. GADTs are considered abstract types. #195
- Fixed incorrectly rejected interfaces with absent\partial function contracts in the presence of tuples as return values. #193
- Fixed support for types containing functions. #186
- Fixed wrong syntax errors in patterns. #181
- Fixed wrong invalid patterns over
unit values. #174 - Fixed the error message for pattern type errors. #172
Internals
- Display the backtrace of an error when
$GOSPELDEBUG is set #295 - Fixed the order of exceptional postconditions in the AST. #200
- Refactored the error handling: Gospel now only raises a single
Gospel.Error exception. #189 - Fixed the representation for type variables in
ts_tuple and fs_tuple. #183 - Added
int as a primitive type. #171 - Refactored
Tterm and Symbols. #85 - Redefined the
ghost type. #155 - Removed the
Pty_open type constructor #109
0.1.0 (11-03-2021)