asai 0.3.0 · OCaml Package

The definition of diagnostics and some utility functions.

Types

type severity =

| Hint
(*
This corresponds to the Hint severity level from LSP (Language Server Protocol). The official specification did not give much guidance on the difference between this level and Info. However, according to the LSP developers, "the idea of the hint severity" is that "for example we in VS Code don't render in the UI as squiggles." They are often used to indicate code smell, along with edit suggestions to fix it.
*)
| Info
(*
This corresponds to the Information severity level from LSP (Language Server Protocol). The official specification did not give much guidance on the difference between this level and Hint.
*)
| Warning
(*
Something went wrong or looked suspicious, but the end user (the user of your proof assistant or compiler) may choose to ignore the issue. For example, maybe some named arguments were not used in a definition.
*)
| Error
(*
A serious error caused by the end user (the user of your proof assistant or compiler) or other external factors (e.g., internet not working).
*)
| Bug
(*
A serious error likely caused by a bug in the proof assistant. You would want the end user to report the bug back to you. This is useful for indicating that certain branches in a pattern matching should be "impossible", while printing out debugging information in case the program logic is flawed.
*)

The type of severity.

type text = Format.formatter -> unit

The type of texts.

When we render a diagnostic, the layout engine of the diagnostic handler should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a text is defined to be a function that takes a formatter and uses it to render the content. A valid text must satisfy the following two conditions:

All string (and character) literals must be encoded using UTF-8.
All string (and character) literals must not contain control characters (such as the newline character \n). It is okay to have break hints (such as @, and @ ) but not literal control characters. This means you should avoid pre-formatted strings, and if you must use them, use text to convert newline characters. Control characters include `U+0000-001F` (C0 controls), `U+007F` (backspace) and `U+0080-009F` (C1 controls). These characters are banned because they would mess up the cursor position.

Pro-tip: to format a text in another text, use %t:

let t = textf "@[<2>this is what the master said:@ @[%t@]@]" inner_text

type loctext = text Range.located

A loctext is a text with location information. "loctext" is a portmanteau of "locate" and "text".

type backtrace = loctext Bwd.bwd

A backtrace is a (backward) list of loctexts.

type 'message t = {

severity : severity;
(*
Severity of the diagnostic.
*)
message : 'message;
(*
The (structured) message.
*)
explanation : loctext;
(*
The free-form explanation.
*)
backtrace : backtrace;
(*
The backtrace leading to this diagnostic.
*)
extra_remarks : loctext Bwd.bwd;
(*
Additional remarks that are relevant to the main message but not part of the backtrace. It is a backward list so that new remarks can be added to its end easily.
*)

}

The type of diagnostics.

Constructing Messages

val text : string -> text

text str converts the string str into a text, converting each '\n' into a call to Format.pp_force_newline.

val textf : ('a, Format.formatter, unit, text) format4 -> 'a

textf format ... formats a text. It is an alias of Format.dprintf. Note that there should not be any literal control characters (e.g., literal newline characters).

val ktextf : (text -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a

ktextf kont format ... is kont (textf format ...). It is an alias of Format.kdprintf.

val loctext : ?loc:Range.t -> string -> loctext

loctext str converts the string str into a loctext.

parameter loc
The location of the loctext (usually the code) to highlight.

val loctextf : 
  ?loc:Range.t ->
  ('a, Format.formatter, unit, loctext) format4 ->
  'a

loctextf format ... constructs a loctext. Note that there should not be any literal control characters (e.g., literal newline characters).

parameter loc
The location of the loctext (usually the code) to highlight.

val kloctextf : 
  ?loc:Range.t ->
  (loctext -> 'b) ->
  ('a, Format.formatter, unit, 'b) format4 ->
  'a

kloctextf kont format ... is kont (loctextf format ...).

parameter loc
The location of the loctext (usually the code) to highlight.

Constructing Diagnostics

val of_text : 
  ?loc:Range.t ->
  ?backtrace:backtrace ->
  ?extra_remarks:loctext list ->
  severity ->
  'message ->
  text ->
  'message t

of_text severity message text constructs a diagnostic from a text.

Example:

of_text Warning ChiError @@ text "your Ch'i is critically low"

parameter backtrace
The backtrace (to overwrite the accumulative frames up to this point).

parameter extra_remarks
Additional remarks that are not part of the backtrace.

since 0.2.0

val of_loctext : 
  ?backtrace:backtrace ->
  ?extra_remarks:loctext list ->
  severity ->
  'message ->
  loctext ->
  'message t

of_loctext severity message loctext constructs a diagnostic from a loctext.

Example:

of_loctext Warning ChiError @@ loctext "your Ch'i is critically low"

parameter backtrace
The backtrace (to overwrite the accumulative frames up to this point).

parameter extra_remarks
Additional remarks that are not part of the backtrace.

val make : 
  ?loc:Range.t ->
  ?backtrace:backtrace ->
  ?extra_remarks:loctext list ->
  severity ->
  'message ->
  string ->
  'message t

make severity message loctext constructs a diagnostic with the loctext.

Example:

make Warning ChiError "your Ch'i is critically low"

parameter backtrace
The backtrace (to overwrite the accumulative frames up to this point).

parameter extra_remarks
Additional remarks that are not part of the backtrace.

val makef : 
  ?loc:Range.t ->
  ?backtrace:backtrace ->
  ?extra_remarks:loctext list ->
  severity ->
  'message ->
  ('a, Format.formatter, unit, 'message t) format4 ->
  'a

makef severity message format ... is of_loctext severity message (loctextf format ...). It formats the message and constructs a diagnostic out of it.

Example:

makef Warning ChiError "your %s is critically low" "Ch'i"

parameter loc
The location of the text (usually the code) to highlight.

parameter backtrace
The backtrace (to overwrite the accumulative frames up to this point).

parameter extra_remarks
Additional remarks that are not part of the backtrace.

val kmakef : 
  ?loc:Range.t ->
  ?backtrace:backtrace ->
  ?extra_remarks:loctext list ->
  ('message t -> 'b) ->
  severity ->
  'message ->
  ('a, Format.formatter, unit, 'b) format4 ->
  'a

kmakef kont severity message format ... is kont (makef severity message format ...).

parameter loc
The location of the text (usually the code) to highlight.

parameter backtrace
The backtrace (to overwrite the accumulative frames up to this point).

parameter extra_remarks
Additional remarks that are not part of the backtrace.

Other Helper Functions

val map : ('message1 -> 'message2) -> 'message1 t -> 'message2 t

A convenience function that maps the message of a diagnostic. This is helpful when using Reporter.S.adopt.

val string_of_text : text -> string

A convenience function that converts a text into a string by formatting it with the maximum admissible margin and then replacing newlines and indentation with a space character.

package asai

Types

Constructing Messages

Constructing Diagnostics

Other Helper Functions