Up – Package index » gospel » CHANGESCreated 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) Make the type-checker save type information in a file #376 Make the with necessary when declaring type invariants #372 and #374 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 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 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.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 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