CHANGES.md

Unreleased

Added

• Add support for mutually recursive ghost types #403

Improved

• Check for repeated name of module and module types #444
• Fix bug in creation of fresh type variables #435
• Fix typing of pattern with inlined record #429
• Remove support for the record update syntax #428
• Rewrote the Gospel standard library to focus on the definition of mathematical objects. [#423] (#423)
• Fix typing of expression with inlined record #420
• Improve error message for unbound record fields #419
• Collect all the missing fields in a record definition and don't accept incomplete record pattern syntax that OCaml consider incorrect #418
• Display proper error message for a number of unsupported construction #406
• Display an error message when encountering a Functor application #404
• Changed the gospel typechecker to use bool as the type of logical formulae #391

Internals

• Extract and document typing environment #447
• Add documentation to Symbols and Ttypes modules #445
• Add documentation and refactor Tmodule #442

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

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
• Added paths to gospel identifiers. #396

0.1.0 (11-03-2021)

• Initial release