FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Improving internal error API #3453

Closed mtzguido closed 3 weeks ago

mtzguido commented 3 weeks ago

The main improvement is that log_issue and raise_error are now uniform, and more flexible. The first argument is always a "position" which is anything from which we can obtain a range (e.g. an actual range, a term, an environment, etc). The last arg is the message, which can be a string or a list of documents. The variants raise_error_doc, raise_error_text, etc, are gone (except for OCaml code, but they are not used internally).

val raise_error
  (#pos_t:Type) {| hasRange pos_t |} (pos : pos_t) // A "position", of any type with a range
  (code : error_code) // An error code
  (#msg_t:_) {| is_error_message msg_t |} (msg : msg_t) // A "message", currently can be a 'string' or 'list document'
  : 'a

val log_issue
  (#pos_t:Type) {| hasRange pos_t |} (pos : pos_t) // A "position", of any type with a range
  (code : error_code) // An error code
  (#msg_t:_) {| is_error_message msg_t |} (msg : msg_t) // A "message", currently can be a 'string' or 'list document'
  : unit
mtzguido commented 3 weeks ago

Also, the Err exception is now gone. We just use Error which has an optional range already.