package gospel

0.3

Added

• Created a gallery of Gospel examples that might serve as a working ground to experiment with Gospel syntax and future extensions of the language. [#361] (https://github.com/ocaml-gospel/gospel/pull/361)

Improved

• Make the type-checker save type information in a file #376
• Make the with necessary when declaring type invariants #372 and #374

Internals

• Fix premature parsing of specification keywords in the preprocessor. #394
• Fix ls_name of unit logical symbol to be () #387
• Fix the is_ts_tuple function so that it doesn't take unit to be a tuple #386
• Use unique identifiers rather than physical equality for Symbols.ls_equal #380
• Remove the gospel_expected prologue at the end of successful tests #363

0.2

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)

• Initial release