+
+ OCaml package documentation
+-
+
- asai +
- asai-examples +
- asai-lsp +
Syslib.OperationsReporter.MessageThe module for messages.
val short_code : t -> stringA concise, ideally Google-able string representation of each message from the library.
Syslib.Reportermodule Message : Asai.MinimumSigs.MessageThe module for messages.
val run :
+ ?init_loc:Asai.Range.t ->
+ ?init_backtrace:Asai.Diagnostic.backtrace ->
+ emit:(Message.t Asai.Diagnostic.t -> unit) ->
+ fatal:(Message.t Asai.Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'arun ~emit ~fatal f runs the thunk f, using emit to handle non-fatal diagnostics before continuing the computation, and fatal to handle fatal diagnostics that have aborted the computation. The recommended way to handle messages from a library that uses asai is to use adopt:
Reporter.adopt (Diagnostic.map message_mapper) The_library.Reporter.run @@ fun () -> ...Syslibmodule Reporter : Asai.MinimumSigs.Reportermodule Operations : sig ... endThe entry point of this library is the module: Syslib.
Make.Messageval short_code : t -> stringA concise, ideally Google-able string representation of each message from the library.
Asai_lsp.MakeThis module provides a rudimentary and incomplete implementation of the LSP protocol.
Note: many features are missing and it does not handle positionEncoding.
module Message : Asai.MinimumSigs.Messageval start :
+ source:string option ->
+ init:(root:string option -> unit) ->
+ load_file:(display:(Message.t Asai.Diagnostic.t -> unit) -> string -> unit) ->
+ unitrun ~init ~load_file starts the LSP server with the two callbacks init and load_file.
Asai_lspmodule Make (Message : Asai.MinimumSigs.Message) : sig ... endThis module provides a rudimentary and incomplete implementation of the LSP protocol.
The entry point of this library is the module: Asai_lsp.
Asai.DiagnosticThe definition of diagnostics and some utility functions.
type severity = | HintThis 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.
| InfoThis 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.
| WarningSomething 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.
*)| ErrorA serious error caused by the end user (the user of your proof assistant or compiler) or other external factors (e.g., internet not working).
*)| BugA 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.
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:
\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_texttype loctext = text Range.locatedA loctext is a text with location information. "loctext" is a portmanteau of "locate" and "text".
type backtrace = loctext Bwd.bwdA 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.
val text : string -> texttext str converts the string str into a text, converting each '\n' into a call to Format.pp_force_newline.
val textf : ('a, Stdlib.Format.formatter, unit, text) Stdlib.format4 -> 'atextf 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, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'aktextf kont format ... is kont (textf format ...). It is an alias of Format.kdprintf.
val loctextf :
+ ?loc:Range.t ->
+ ('a, Stdlib.Format.formatter, unit, loctext) Stdlib.format4 ->
+ 'aloctextf format ... constructs a loctext. Note that there should not be any literal control characters (e.g., literal newline characters).
val kloctextf :
+ ?loc:Range.t ->
+ (loctext -> 'b) ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'akloctextf kont format ... is kont (loctextf format ...).
val of_text :
+ ?loc:Range.t ->
+ ?backtrace:backtrace ->
+ ?extra_remarks:loctext list ->
+ severity ->
+ 'message ->
+ text ->
+ 'message tof_text severity message text constructs a diagnostic from a text.
Example:
of_text Warning ChiError @@ text "your Ch'i is critically low"val of_loctext :
+ ?backtrace:backtrace ->
+ ?extra_remarks:loctext list ->
+ severity ->
+ 'message ->
+ loctext ->
+ 'message tof_loctext severity message loctext constructs a diagnostic from a loctext.
Example:
of_loctext Warning ChiError @@ loctext "your Ch'i is critically low"val make :
+ ?loc:Range.t ->
+ ?backtrace:backtrace ->
+ ?extra_remarks:loctext list ->
+ severity ->
+ 'message ->
+ string ->
+ 'message tmake severity message loctext constructs a diagnostic with the loctext.
Example:
make Warning ChiError "your Ch'i is critically low"val makef :
+ ?loc:Range.t ->
+ ?backtrace:backtrace ->
+ ?extra_remarks:loctext list ->
+ severity ->
+ 'message ->
+ ('a, Stdlib.Format.formatter, unit, 'message t) Stdlib.format4 ->
+ 'amakef 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"val kmakef :
+ ?loc:Range.t ->
+ ?backtrace:backtrace ->
+ ?extra_remarks:loctext list ->
+ ('message t -> 'b) ->
+ severity ->
+ 'message ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'akmakef kont severity message format ... is kont (makef severity message format ...).
A convenience function that maps the message of a diagnostic. This is helpful when using Reporter.S.adopt.
Asai.ExplicationThe definition of highlighted text suitable for rendering. You probably do not need this module unless you want to create your own diagnostic handler.
A segment is an optionally tagged string from the user content. (Note the use of option.)
type 'tag block = {begin_line_num : int;The starting 1-indexed line number of a block.
*)end_line_num : int;The ending 1-indexed line number of a block.
*)lines : 'tag line list;}A block is a collection of consecutive lines.
type 'tag part = {source : Range.source;The source of a part.
*)blocks : 'tag block list;The blocks within a part.
*)}A part consists of multiple blocks from the same file. These blocks should be non-overlapping and sorted by importance or the textual order.
type 'tag t = 'tag part listHighlighted texts.
val dump :
+ (Stdlib.Format.formatter -> 'tag -> unit) ->
+ Stdlib.Format.formatter ->
+ 'tag t ->
+ unitUgly printer for debugging
Make.Tagval priority : t -> intGet the priority number of a tag. We followed the UNIX convention here---a smaller priority number represents higher priority. The convention works well with List.sort, which sorts numbers in ascending order. (The more important things go first.)
val dump : Stdlib.Format.formatter -> t -> unitUgly printer for debugging
Explicator.MakeMaking an explicator.
val explicate :
+ ?line_breaks:[ `Unicode | `Traditional ] ->
+ ?block_splitting_threshold:int ->
+ ?blend:(Tag.t -> Tag.t -> Tag.t) ->
+ ?debug:bool ->
+ (Tag.t * Range.t) list ->
+ Tag.t Explication.tExplicate a list of ranges using content from a data reader. This function must be run under SourceReader.run.
Asai.ExplicatorTurning location information into highlighted text suitable for rendering. You probably do not need this module unless you want to create your own diagnostic handler.
exception Invalid_range of Range.t
+ * [ `Begin of
+ [ `Offset of
+ [ `Negative of int
+ | `Beyond_end_of_file of int * int
+ | `Within_newline of int * (int * int) ]
+ | `Incorrect_start_of_line of int * int
+ | `Incorrect_line_num of int * int ]
+ | `End of
+ [ `Offset of
+ [ `Negative of int
+ | `Beyond_end_of_file of int * int
+ | `Within_newline of int * (int * int) ]
+ | `Incorrect_start_of_line of int * int
+ | `Incorrect_line_num of int * int ]
+ | `End_of_file of
+ [ `Offset of
+ [ `Negative of int
+ | `Beyond_end_of_file of int * int
+ | `Within_newline of int * (int * int) ]
+ | `Incorrect_start_of_line of int * int
+ | `Incorrect_line_num of int * int ]
+ | `Not_end_of_file of int * int ]Invalid_range (range, reason) means that range is an invalid range because of reason. This exception will be raised only when the debug mode is enabled. See the debug argument of Explicator.S.explicate.
module type Tag = sig ... endThe signature of tags
module type S = sig ... endThe signature of explicators.
The default tag blending algorithm that chooses the more important tag based on priority.
S.Tagval priority : t -> intGet the priority number of a tag. We followed the UNIX convention here---a smaller priority number represents higher priority. The convention works well with List.sort, which sorts numbers in ascending order. (The more important things go first.)
val dump : Stdlib.Format.formatter -> t -> unitUgly printer for debugging
Explicator.SThe signature of explicators.
val explicate :
+ ?line_breaks:[ `Unicode | `Traditional ] ->
+ ?block_splitting_threshold:int ->
+ ?blend:(Tag.t -> Tag.t -> Tag.t) ->
+ ?debug:bool ->
+ (Tag.t * Range.t) list ->
+ Tag.t Explication.tExplicate a list of ranges using content from a data reader. This function must be run under SourceReader.run.
Explicator.TagThe signature of tags
val priority : t -> intGet the priority number of a tag. We followed the UNIX convention here---a smaller priority number represents higher priority. The convention works well with List.sort, which sorts numbers in ascending order. (The more important things go first.)
val dump : Stdlib.Format.formatter -> t -> unitUgly printer for debugging
Make.Messageval default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
GitHub.MakeThe functor to create a printer for GitHub Actions workflow commands.
module Message : Reporter.Messageval print : Message.t Diagnostic.t -> unitPrint a diagnostic as a GitHub Actions workflow command. Only the main explanation will be printed; backtraces and extra remarks are ignored. Column numbers are also ignored because GitHub does not seem to use them.
Example output:
::error file=examples/stlc/example.lambda,line=2,endLine=2,title=E002::Variable 'x' is not in scope
Asai.GitHubGitHub Actions workflow commands.
module Make (Message : Reporter.Message) : sig ... endThe functor to create a printer for GitHub Actions workflow commands.
Asai.MinimumSigsSignatures that specify the minimum interface for libraries, applications, and handlers to work together.
module type Message = sig ... endThe minimum interface to use diagnostic handlers.
module type Reporter = sig ... endThe minimum interface for libraries and applications to work together.
MinimumSigs.MessageThe minimum interface to use diagnostic handlers.
Any module implementing Reporter.Message or StructuredReporter.Message will also implement this minimum interface.
val short_code : t -> stringA concise, ideally Google-able string representation of each message from the library.
Reporter.MessageThe module for messages.
val short_code : t -> stringA concise, ideally Google-able string representation of each message from the library.
MinimumSigs.ReporterThe minimum interface for libraries and applications to work together.
If you are the author of a library that uses asai, it is recommended to wrap your reporter with this signature in the wrapper. For example, if you are using Dune, and your wrapper file is CoolLibrary.ml(i), use this to wrap your Reporter:
module Reporter : Asai.MinimumSigs.ReporterIf you arrive here because the library you are using employs this template signature to reveal only the minimum API, you can write the following code to connect the library's reporter to yours:
Reporter.adopt (Diagnostic.map message_mapper) CoolLibrary.Reporter.run @@ fun () -> ...Please take a look at our Quick Start Tutorial about how to use a library that uses asai.
val run :
+ ?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:(Message.t Diagnostic.t -> unit) ->
+ fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'arun ~emit ~fatal f runs the thunk f, using emit to handle non-fatal diagnostics before continuing the computation, and fatal to handle fatal diagnostics that have aborted the computation. The recommended way to handle messages from a library that uses asai is to use adopt:
Reporter.adopt (Diagnostic.map message_mapper) The_library.Reporter.run @@ fun () -> ...Asai.RangeLocations and ranges.
type string_source = {title : string option;The title of a string source. A diagnostic handler can use the title of a string source in lieu of a file path.
*)content : string;The content of a string source
*)}The string source of a position or a range.
type source = [ | `File of stringA file source specified by its file path.
*)| `String of string_sourceA string (in-memory) source.
*) ]The source of a position or a range. The `String source can be used for representing inputs in REPL.
type position = {source : source;The source (e.g., the file) that contains the position.
*)offset : int;The 0-indexed byte offset of the position relative to the beginning of the source.
*)start_of_line : int;The 0-indexed byte offset pointing to the start of the line that contains the position.
*)line_num : int;The 1-indexed line number of the line that contains the position.
*)}The type of positions; this is isomorphic to Lexing.position, but with arguably better field names.
An auxiliary type to package data with an optional range.
make (beginning, ending) builds the range [beginning, ending) (not including the byte at the ending position) from a pair of positions beginning and ending. A range is empty if its beginning and ending positions are the same.
eof pos builds a special range referring to the end of the source. The input pos must be pointing at the end position; for example, if the position referring to a string source, pos.offset should be the length of the string.
view range returns a view of the range.
split range returning the pair of the beginning and ending positions of range. It is the left-inverse of make.
val begin_line_num : t -> intbegin_line_num range returns the 1-indexed line number of the beginning position.
val end_line_num : t -> intend_line_num range returns the 1-indexed line number of the ending position.
val begin_offset : t -> intbegin_offset range returns the 0-indexed offset of the (inclusive) beginning position.
val end_offset : t -> intend_offset range returns the 0-indexed offset of the (exclusive) ending position.
val title : source -> string optiontitle src gets the title of a string source or the path of a file source, or None if it does not exist.
of_lex_position pos converts an OCaml lexer position pos of type Lexing.position into a position. The input pos must be byte-indexed. (Therefore, the OCaml tool ocamllex is compatible, but the OCaml library sedlex is not because it uses Unicode code points.)
of_lex_range (begining, ending) takes a pair of OCaml lexer positions and creates a range. It is make (of_lex_position begining, of_lex_position ending).
of_lexbuf lexbuf constructs a range from the current lexeme that lexbuf points to. It is of_lex_range (Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf).
val locate_lex :
+ ?source:source ->
+ (Stdlib.Lexing.position * Stdlib.Lexing.position) ->
+ 'a ->
+ 'a locatedlocate_lex ps v is a helper function to create a value annotated with a range. It is locate (Some (of_lex_range ps)) v and is designed to work with the OCaml parser generator Menhir. You can add the following code to your Menhir grammar to generate annotated data:
%inline
+locate(X):
+ | e = X
+ { Asai.Range.locate_lex $loc e }Ugly printer for debugging
val dump_source : Stdlib.Format.formatter -> source -> unitval dump_position : Stdlib.Format.formatter -> position -> unitval dump : Stdlib.Format.formatter -> t -> unitMake.Messageval default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
Reporter.MakeThe functor to generate a reporter.
val emit :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ unitemit message explanation emits the explanation and continues the computation.
Example:
Reporter.emit TypeError "the type `nat' is extremely unnatural"val emitf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 ->
+ 'aemitf message format ... formats and emits a message, and then continues the computation. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.emitf TypeError "type %a is too ugly" Syntax.pp tpval emit_diagnostic : Message.t Diagnostic.t -> unitEmit a diagnostic and continue the computation.
val fatal :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ 'afatal message explanation aborts the current computation with the explanation.
Example:
Reporter.fatal CatError "forgot to feed the cat"val fatalf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'afatalf message format ... constructs a diagnostic and aborts the current computation with the diagnostic. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.fatalf SecurityTooStrict "failed to write the password %s on the screen" passwordval fatal_diagnostic : Message.t Diagnostic.t -> 'aAbort the computation with a diagnostic.
val get_backtrace : unit -> Diagnostic.backtraceget_backtrace() returns the current backtrace.
val with_backtrace : Diagnostic.backtrace -> (unit -> 'a) -> 'awith_backtrace bt f runs the thunk f with bt as the initial backtrace.
Example:
(* running code with a fresh backtrace *)
+with_backtrace Emp @@ fun () -> ...val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'atrace str f records the string str and runs the thunk f with the new backtrace.
val tracef :
+ ?loc:Range.t ->
+ ('a, Stdlib.Format.formatter, unit, (unit -> 'b) -> 'b) Stdlib.format4 ->
+ 'atracef format ... f formats and records a frame in the backtrace, and runs the thunk f with the new backtrace. Note that there should not be any literal control characters. See Diagnostic.text.
val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'atrace_text text f records the text and runs the thunk f with the new backtrace.
val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'aval get_loc : unit -> Range.t optionval with_loc : Range.t option -> (unit -> 'a) -> 'aval merge_loc : Range.t option -> (unit -> 'a) -> 'amerge_loc loc f "merges" loc into the current default location for emit and fatal and runs the thunk f. By "merge", it means that if loc is None, then the current default location is kept; otherwise, it is overwritten. Note that with_loc None will clear the current default location, while merge_loc None will keep it. See with_loc.
Functions in this section differ from the ones in Diagnostic (for example, Diagnostic.make) in that they fill out the current location, the current backtrace, and the severity automatically. (One can still overwrite them with optional arguments.)
val diagnostic :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ Message.t Diagnostic.tdiagnostic message explanation constructs a diagnostic with the explanation along with the backtrace frames recorded via trace.
Example:
Reporter.diagnostic SyntaxError "too many emojis"val diagnosticf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, Message.t Diagnostic.t) Stdlib.format4 ->
+ 'adiagnosticf message format ... constructs a diagnostic along with the backtrace frames recorded via trace. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.diagnosticf TypeError "term %a does not type check, maybe" Syntax.pp tmval kdiagnosticf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ (Message.t Diagnostic.t -> 'b) ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'akdiagnosticf kont message format ... is kont (diagnosticf message format ...). Note that there should not be any literal control characters. See Diagnostic.text.
val run :
+ ?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:(Message.t Diagnostic.t -> unit) ->
+ fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval adopt :
+ ('message Diagnostic.t -> Message.t Diagnostic.t) ->
+ (?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:('message Diagnostic.t -> unit) ->
+ fatal:('message Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'a) ->
+ (unit -> 'a) ->
+ 'aadopt m run f runs the thunk f that uses a different Reporter instance. It takes the runner run from that Reporter instance as an argument to handle effects, and will use m to transform diagnostics generated by f into ones in the current Reporter instance. The backtrace within f will include the backtrace that leads to adopt, and the innermost specified location will be carried over, too. The intended use case is to integrate diagnostics from a library into those in the main application.
adopt is a convenience function that can be implemented as follows:
let adopt m f run =
+ run
+ ?init_loc:(get_loc())
+ ?init_backtrace:(Some (get_backtrace()))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ fHere shows the intended usage, where Cool_lib is the library to be used in the main application:
Reporter.adopt (Diagnostic.map message_mapper) Cool_lib.Reporter.run @@ fun () -> ...val try_with :
+ ?emit:(Message.t Diagnostic.t -> unit) ->
+ ?fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval map_diagnostic :
+ (Message.t Diagnostic.t -> Message.t Diagnostic.t) ->
+ (unit -> 'a) ->
+ 'amap_diagnostic m f runs the thunk f and applies m to any diagnostic sent by f. It is a convenience function that can be implemented as follows:
let map_diagnostic m f =
+ try_with
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ fval register_printer :
+ ([ `Trace
+ | `Emit of Message.t Diagnostic.t
+ | `Fatal of Message.t Diagnostic.t ] ->
+ string option) ->
+ unitregister_printer p registers a printer p via Printexc.register_printer to convert unhandled internal effects and exceptions into strings for the OCaml runtime system to display. Ideally, all internal effects and exceptions should have been handled by run and there is no need to use this function, but when it is not the case, this function can be helpful for debugging. The functor Reporter.Make always registers a simple printer to suggest using run, but you can register new ones to override it. The return type of the printer p should return Some s where s is the resulting string, or None if it chooses not to convert a particular effect or exception. The registered printers are tried in reverse order until one of them returns Some s for some s; that is, the last registered printer is tried first. Note that this function is a wrapper of Printexc.register_printer and all the registered printers (via this function or Printexc.register_printer) are put into the same list.
The input type of the printer p is a variant representation of all internal effects and exceptions used in this module:
`Trace corresponds to the effect triggered by trace; and`Emit diag corresponds to the effect triggered by emit; and`Fatal diag corresponds to the exception triggered by fatal.Note: Diagnostic.string_of_text can be handy for converting a text into a string.
Asai.ReporterGenerating and handling diagnostics using algebraic effects. The API is optimized for attaching free-form text.
The signature of a reporter.
module type Message = sig ... endThe signature of messages. An implementer should specify the message type used in their library or application.
module type S = sig ... endReporter.MessageThe signature of messages. An implementer should specify the message type used in their library or application.
val default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
S.Messageval default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
Reporter.Sval emit :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ unitemit message explanation emits the explanation and continues the computation.
Example:
Reporter.emit TypeError "the type `nat' is extremely unnatural"val emitf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 ->
+ 'aemitf message format ... formats and emits a message, and then continues the computation. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.emitf TypeError "type %a is too ugly" Syntax.pp tpval emit_diagnostic : Message.t Diagnostic.t -> unitEmit a diagnostic and continue the computation.
val fatal :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ 'afatal message explanation aborts the current computation with the explanation.
Example:
Reporter.fatal CatError "forgot to feed the cat"val fatalf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'afatalf message format ... constructs a diagnostic and aborts the current computation with the diagnostic. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.fatalf SecurityTooStrict "failed to write the password %s on the screen" passwordval fatal_diagnostic : Message.t Diagnostic.t -> 'aAbort the computation with a diagnostic.
val get_backtrace : unit -> Diagnostic.backtraceget_backtrace() returns the current backtrace.
val with_backtrace : Diagnostic.backtrace -> (unit -> 'a) -> 'awith_backtrace bt f runs the thunk f with bt as the initial backtrace.
Example:
(* running code with a fresh backtrace *)
+with_backtrace Emp @@ fun () -> ...val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'atrace str f records the string str and runs the thunk f with the new backtrace.
val tracef :
+ ?loc:Range.t ->
+ ('a, Stdlib.Format.formatter, unit, (unit -> 'b) -> 'b) Stdlib.format4 ->
+ 'atracef format ... f formats and records a frame in the backtrace, and runs the thunk f with the new backtrace. Note that there should not be any literal control characters. See Diagnostic.text.
val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'atrace_text text f records the text and runs the thunk f with the new backtrace.
val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'aval get_loc : unit -> Range.t optionval with_loc : Range.t option -> (unit -> 'a) -> 'aval merge_loc : Range.t option -> (unit -> 'a) -> 'amerge_loc loc f "merges" loc into the current default location for emit and fatal and runs the thunk f. By "merge", it means that if loc is None, then the current default location is kept; otherwise, it is overwritten. Note that with_loc None will clear the current default location, while merge_loc None will keep it. See with_loc.
Functions in this section differ from the ones in Diagnostic (for example, Diagnostic.make) in that they fill out the current location, the current backtrace, and the severity automatically. (One can still overwrite them with optional arguments.)
val diagnostic :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ string ->
+ Message.t Diagnostic.tdiagnostic message explanation constructs a diagnostic with the explanation along with the backtrace frames recorded via trace.
Example:
Reporter.diagnostic SyntaxError "too many emojis"val diagnosticf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, Message.t Diagnostic.t) Stdlib.format4 ->
+ 'adiagnosticf message format ... constructs a diagnostic along with the backtrace frames recorded via trace. Note that there should not be any literal control characters. See Diagnostic.text.
Example:
Reporter.diagnosticf TypeError "term %a does not type check, maybe" Syntax.pp tmval kdiagnosticf :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ (Message.t Diagnostic.t -> 'b) ->
+ Message.t ->
+ ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
+ 'akdiagnosticf kont message format ... is kont (diagnosticf message format ...). Note that there should not be any literal control characters. See Diagnostic.text.
val run :
+ ?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:(Message.t Diagnostic.t -> unit) ->
+ fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval adopt :
+ ('message Diagnostic.t -> Message.t Diagnostic.t) ->
+ (?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:('message Diagnostic.t -> unit) ->
+ fatal:('message Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'a) ->
+ (unit -> 'a) ->
+ 'aadopt m run f runs the thunk f that uses a different Reporter instance. It takes the runner run from that Reporter instance as an argument to handle effects, and will use m to transform diagnostics generated by f into ones in the current Reporter instance. The backtrace within f will include the backtrace that leads to adopt, and the innermost specified location will be carried over, too. The intended use case is to integrate diagnostics from a library into those in the main application.
adopt is a convenience function that can be implemented as follows:
let adopt m f run =
+ run
+ ?init_loc:(get_loc())
+ ?init_backtrace:(Some (get_backtrace()))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ fHere shows the intended usage, where Cool_lib is the library to be used in the main application:
Reporter.adopt (Diagnostic.map message_mapper) Cool_lib.Reporter.run @@ fun () -> ...val try_with :
+ ?emit:(Message.t Diagnostic.t -> unit) ->
+ ?fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval map_diagnostic :
+ (Message.t Diagnostic.t -> Message.t Diagnostic.t) ->
+ (unit -> 'a) ->
+ 'amap_diagnostic m f runs the thunk f and applies m to any diagnostic sent by f. It is a convenience function that can be implemented as follows:
let map_diagnostic m f =
+ try_with
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ fval register_printer :
+ ([ `Trace
+ | `Emit of Message.t Diagnostic.t
+ | `Fatal of Message.t Diagnostic.t ] ->
+ string option) ->
+ unitregister_printer p registers a printer p via Printexc.register_printer to convert unhandled internal effects and exceptions into strings for the OCaml runtime system to display. Ideally, all internal effects and exceptions should have been handled by run and there is no need to use this function, but when it is not the case, this function can be helpful for debugging. The functor Reporter.Make always registers a simple printer to suggest using run, but you can register new ones to override it. The return type of the printer p should return Some s where s is the resulting string, or None if it chooses not to convert a particular effect or exception. The registered printers are tried in reverse order until one of them returns Some s for some s; that is, the last registered printer is tried first. Note that this function is a wrapper of Printexc.register_printer and all the registered printers (via this function or Printexc.register_printer) are put into the same list.
The input type of the printer p is a variant representation of all internal effects and exceptions used in this module:
`Trace corresponds to the effect triggered by trace; and`Emit diag corresponds to the effect triggered by emit; and`Fatal diag corresponds to the exception triggered by fatal.Note: Diagnostic.string_of_text can be handy for converting a text into a string.
Asai.SourceReaderReading the source content. It uses memory-mapped I/O for files. You probably do not need this module unless you want to create your own diagnostic handler.
val load : Range.source -> sourceload source loads the source.
val length : source -> intlength source gets the size of the source content.
val unsafe_get : source -> int -> charunsafe_get source i reads the ith byte of the file without checking the file size.
Make.Messageval default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val default_text : t -> Diagnostic.textThe default text of the message. This is the long explanation of the message that the end user would see. You might find helper functions Diagnostic.text and Diagnostic.textf useful. The text may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
StructuredReporter.MakeThe functor to generate a reporter.
val emit :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ unitemit message emits the message and continues the computation.
Example:
Reporter.emit @@ TypeError (tm, ty)val emit_diagnostic : Message.t Diagnostic.t -> unitEmit a diagnostic and continue the computation.
val fatal :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ 'afatal message aborts the current computation with the message.
Example:
Reporter.fatal @@ CatError "forgot to feed the cat"val fatal_diagnostic : Message.t Diagnostic.t -> 'aAbort the computation with a diagnostic.
val get_backtrace : unit -> Diagnostic.backtraceget_backtrace() returns the current backtrace.
val with_backtrace : Diagnostic.backtrace -> (unit -> 'a) -> 'awith_backtrace bt f runs the thunk f with bt as the initial backtrace.
Example:
(* running code with a fresh backtrace *)
+with_backtrace Emp @@ fun () -> ...val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'atrace str f records the string str and runs the thunk f with the new backtrace.
val tracef :
+ ?loc:Range.t ->
+ ('a, Stdlib.Format.formatter, unit, (unit -> 'b) -> 'b) Stdlib.format4 ->
+ 'atracef format ... f formats and records a frame in the backtrace, and runs the thunk f with the new backtrace. Note that there should not be any literal control characters. See Diagnostic.text.
val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'atrace_text text f records the text and runs the thunk f with the new backtrace.
val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'aval get_loc : unit -> Range.t optionval with_loc : Range.t option -> (unit -> 'a) -> 'aval merge_loc : Range.t option -> (unit -> 'a) -> 'amerge_loc loc f "merges" loc into the current default location for emit and fatal and runs the thunk f. By "merge", it means that if loc is None, then the current default location is kept; otherwise, it is overwritten. Note that with_loc None will clear the current default location, while merge_loc None will keep it. See with_loc.
Functions in this section differ from the ones in Diagnostic (for example, Diagnostic.make) in that they fill out the current location, the current backtrace, and the severity automatically. (One can still overwrite them with optional arguments.)
val diagnostic :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ Message.t Diagnostic.tdiagnostic message constructs a diagnostic with the message along with the backtrace frames recorded via trace.
Example:
Reporter.diagnostic @@ SyntaxError "too many emojis"val run :
+ ?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:(Message.t Diagnostic.t -> unit) ->
+ fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval adopt :
+ ('message Diagnostic.t -> Message.t Diagnostic.t) ->
+ (?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:('message Diagnostic.t -> unit) ->
+ fatal:('message Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'a) ->
+ (unit -> 'a) ->
+ 'aadopt m run f runs the thunk f that uses a different Reporter instance. It takes the runner run from that Reporter instance as an argument to handle effects, and will use m to transform diagnostics generated by f into ones in the current Reporter instance. The backtrace within f will include the backtrace that leads to adopt, and the innermost specified location will be carried over, too. The intended use case is to integrate diagnostics from a library into those in the main application.
adopt is a convenience function that can be implemented as follows:
let adopt m f run =
+ run
+ ?init_loc:(get_loc())
+ ?init_backtrace:(Some (get_backtrace()))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ fHere shows the intended usage, where Cool_lib is the library to be used in the main application:
Reporter.adopt (Diagnostic.map message_mapper) Cool_lib.Reporter.run @@ fun () -> ...val try_with :
+ ?emit:(Message.t Diagnostic.t -> unit) ->
+ ?fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval map_diagnostic :
+ (Message.t Diagnostic.t -> Message.t Diagnostic.t) ->
+ (unit -> 'a) ->
+ 'amap_diagnostic m f runs the thunk f and applies m to any diagnostic sent by f. It is a convenience function that can be implemented as follows:
let map_diagnostic m f =
+ try_with
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ fval register_printer :
+ ([ `Trace
+ | `Emit of Message.t Diagnostic.t
+ | `Fatal of Message.t Diagnostic.t ] ->
+ string option) ->
+ unitregister_printer p registers a printer p via Printexc.register_printer to convert unhandled internal effects and exceptions into strings for the OCaml runtime system to display. Ideally, all internal effects and exceptions should have been handled by run and there is no need to use this function, but when it is not the case, this function can be helpful for debugging. The functor Reporter.Make always registers a simple printer to suggest using run, but you can register new ones to override it. The return type of the printer p should return Some s where s is the resulting string, or None if it chooses not to convert a particular effect or exception. The registered printers are tried in reverse order until one of them returns Some s for some s; that is, the last registered printer is tried first. Note that this function is a wrapper of Printexc.register_printer and all the registered printers (via this function or Printexc.register_printer) are put into the same list.
The input type of the printer p is a variant representation of all internal effects and exceptions used in this module:
`Trace corresponds to the effect triggered by trace; and`Emit diag corresponds to the effect triggered by emit; and`Fatal diag corresponds to the exception triggered by fatal.Note: Diagnostic.string_of_text can be handy for converting a text into a string.
Asai.StructuredReporterGenerating and handling diagnostics using algebraic effects. The API is optimized for fully structured messages.
The signature of a reporter.
module type Message = sig ... endThe signature of structured messages. An implementer should specify the structured messages used in their library or application.
module type S = sig ... endStructuredReporter.MessageThe signature of structured messages. An implementer should specify the structured messages used in their library or application.
val default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val default_text : t -> Diagnostic.textThe default text of the message. This is the long explanation of the message that the end user would see. You might find helper functions Diagnostic.text and Diagnostic.textf useful. The text may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
S.Messageval default_severity : t -> Diagnostic.severityThe default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the end user should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic.
val default_text : t -> Diagnostic.textThe default text of the message. This is the long explanation of the message that the end user would see. You might find helper functions Diagnostic.text and Diagnostic.textf useful. The text may be overwritten at the time of issuing a diagnostic.
val short_code : t -> stringA concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, E001 works better than type-checking error. It will be assumed that the string representation has no control characters (such as newline characters).
StructuredReporter.Sval emit :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ unitemit message emits the message and continues the computation.
Example:
Reporter.emit @@ TypeError (tm, ty)val emit_diagnostic : Message.t Diagnostic.t -> unitEmit a diagnostic and continue the computation.
val fatal :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ 'afatal message aborts the current computation with the message.
Example:
Reporter.fatal @@ CatError "forgot to feed the cat"val fatal_diagnostic : Message.t Diagnostic.t -> 'aAbort the computation with a diagnostic.
val get_backtrace : unit -> Diagnostic.backtraceget_backtrace() returns the current backtrace.
val with_backtrace : Diagnostic.backtrace -> (unit -> 'a) -> 'awith_backtrace bt f runs the thunk f with bt as the initial backtrace.
Example:
(* running code with a fresh backtrace *)
+with_backtrace Emp @@ fun () -> ...val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'atrace str f records the string str and runs the thunk f with the new backtrace.
val tracef :
+ ?loc:Range.t ->
+ ('a, Stdlib.Format.formatter, unit, (unit -> 'b) -> 'b) Stdlib.format4 ->
+ 'atracef format ... f formats and records a frame in the backtrace, and runs the thunk f with the new backtrace. Note that there should not be any literal control characters. See Diagnostic.text.
val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'atrace_text text f records the text and runs the thunk f with the new backtrace.
val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'aval get_loc : unit -> Range.t optionval with_loc : Range.t option -> (unit -> 'a) -> 'aval merge_loc : Range.t option -> (unit -> 'a) -> 'amerge_loc loc f "merges" loc into the current default location for emit and fatal and runs the thunk f. By "merge", it means that if loc is None, then the current default location is kept; otherwise, it is overwritten. Note that with_loc None will clear the current default location, while merge_loc None will keep it. See with_loc.
Functions in this section differ from the ones in Diagnostic (for example, Diagnostic.make) in that they fill out the current location, the current backtrace, and the severity automatically. (One can still overwrite them with optional arguments.)
val diagnostic :
+ ?severity:Diagnostic.severity ->
+ ?loc:Range.t ->
+ ?text:Diagnostic.text ->
+ ?backtrace:Diagnostic.backtrace ->
+ ?extra_remarks:Diagnostic.loctext list ->
+ Message.t ->
+ Message.t Diagnostic.tdiagnostic message constructs a diagnostic with the message along with the backtrace frames recorded via trace.
Example:
Reporter.diagnostic @@ SyntaxError "too many emojis"val run :
+ ?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:(Message.t Diagnostic.t -> unit) ->
+ fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval adopt :
+ ('message Diagnostic.t -> Message.t Diagnostic.t) ->
+ (?init_loc:Range.t ->
+ ?init_backtrace:Diagnostic.backtrace ->
+ emit:('message Diagnostic.t -> unit) ->
+ fatal:('message Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'a) ->
+ (unit -> 'a) ->
+ 'aadopt m run f runs the thunk f that uses a different Reporter instance. It takes the runner run from that Reporter instance as an argument to handle effects, and will use m to transform diagnostics generated by f into ones in the current Reporter instance. The backtrace within f will include the backtrace that leads to adopt, and the innermost specified location will be carried over, too. The intended use case is to integrate diagnostics from a library into those in the main application.
adopt is a convenience function that can be implemented as follows:
let adopt m f run =
+ run
+ ?init_loc:(get_loc())
+ ?init_backtrace:(Some (get_backtrace()))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ fHere shows the intended usage, where Cool_lib is the library to be used in the main application:
Reporter.adopt (Diagnostic.map message_mapper) Cool_lib.Reporter.run @@ fun () -> ...val try_with :
+ ?emit:(Message.t Diagnostic.t -> unit) ->
+ ?fatal:(Message.t Diagnostic.t -> 'a) ->
+ (unit -> 'a) ->
+ 'aval map_diagnostic :
+ (Message.t Diagnostic.t -> Message.t Diagnostic.t) ->
+ (unit -> 'a) ->
+ 'amap_diagnostic m f runs the thunk f and applies m to any diagnostic sent by f. It is a convenience function that can be implemented as follows:
let map_diagnostic m f =
+ try_with
+ ~fatal:(fun d -> fatal_diagnostic (m d))
+ ~emit:(fun d -> emit_diagnostic (m d))
+ fval register_printer :
+ ([ `Trace
+ | `Emit of Message.t Diagnostic.t
+ | `Fatal of Message.t Diagnostic.t ] ->
+ string option) ->
+ unitregister_printer p registers a printer p via Printexc.register_printer to convert unhandled internal effects and exceptions into strings for the OCaml runtime system to display. Ideally, all internal effects and exceptions should have been handled by run and there is no need to use this function, but when it is not the case, this function can be helpful for debugging. The functor Reporter.Make always registers a simple printer to suggest using run, but you can register new ones to override it. The return type of the printer p should return Some s where s is the resulting string, or None if it chooses not to convert a particular effect or exception. The registered printers are tried in reverse order until one of them returns Some s for some s; that is, the last registered printer is tried first. Note that this function is a wrapper of Printexc.register_printer and all the registered printers (via this function or Printexc.register_printer) are put into the same list.
The input type of the printer p is a variant representation of all internal effects and exceptions used in this module:
`Trace corresponds to the effect triggered by trace; and`Emit diag corresponds to the effect triggered by emit; and`Fatal diag corresponds to the exception triggered by fatal.Note: Diagnostic.string_of_text can be handy for converting a text into a string.
Make.Messageval short_code : t -> stringA concise, ideally Google-able string representation of each message from the library.
Tty.MakeThis module provides functions to display or interact with diagnostics in UNIX terminals.
module Message : MinimumSigs.Messageval display :
+ ?output:Stdlib.out_channel ->
+ ?use_ansi:bool ->
+ ?use_color:bool ->
+ ?show_backtrace:bool ->
+ ?line_breaks:[ `Unicode | `Traditional ] ->
+ ?block_splitting_threshold:int ->
+ ?tab_size:int ->
+ ?debug:bool ->
+ Message.t Diagnostic.t ->
+ unitdisplay d prints the diagnostic d to the standard output, using terminal control characters for formatting. A message will look like this (but with coloring):
￫ warning[hello] + ╭ ￭ /path/to/file.cool + ┆ 1 | aaaaaaaaaa + ┆ 2 | bbbbbbbbbb + ╯ ^ when stepping into the abyss + ￭ /path/to/file.cool + 2 | bbbbbbbbbb + 3 | cccccccccc + ^ could not say hi here
Asai.TtyDiagnostic display for UNIX terminals.
module Make (Message : MinimumSigs.Message) : sig ... endThis module provides functions to display or interact with diagnostics in UNIX terminals.
AsaiCompiler diagnostics
A diagnostic is a message for the end user, for example a compiler warning or error.
module Range : sig ... endLocations and ranges.
module Diagnostic : sig ... endThe definition of diagnostics and some utility functions.
module Reporter : sig ... endGenerating and handling diagnostics using algebraic effects. The API is optimized for attaching free-form text.
module StructuredReporter : sig ... endGenerating and handling diagnostics using algebraic effects. The API is optimized for fully structured messages.
module MinimumSigs : sig ... endSignatures that specify the minimum interface for libraries, applications, and handlers to work together.
These handlers are subject to changes, but we will minimize incompatible changes between minor versions.
module Tty : sig ... endDiagnostic display for UNIX terminals.
module GitHub : sig ... endGitHub Actions workflow commands.
The internals are exposed for convenience, but they are subject to changes between minor versions.
module Explication : sig ... endThe definition of highlighted text suitable for rendering. You probably do not need this module unless you want to create your own diagnostic handler.
module Explicator : sig ... endTurning location information into highlighted text suitable for rendering. You probably do not need this module unless you want to create your own diagnostic handler.
module SourceReader : sig ... endReading the source content. It uses memory-mapped I/O for files. You probably do not need this module unless you want to create your own diagnostic handler.
In addition to the main message, the API should allow an implementer to easily specify the following five factors of a diagnostic, and it should be possible to specify them independently.
V0003. A succinct representation is useful for an end user to report a bug or ask for help.extra_remarks.We realized there are two distinct use modes when coming to message reporting:
We should support at least the free-form use mode, and ideally support both. The free-form reporting is implemented as Reporter and the structured one is implemented as StructuredReporter.
asaiIt should be easy for an application to use other libraries who themselves use asai, even if the application and the library made different choices between free-form and structured reporting. Our current implementation uses the same diagnostic type for both reporting styles and allows an application to adopt diagnostics from a library.
The original design of asai did not retain any location information across API calls. That is, the location used to create a backtrace frame will not be inherited by inner API calls:
Reporter.trace ~loc "outer trace with a location" @@ fun () ->
+Reporter.emit Greeting "hello"
+(* the message ["hello"] originally would not have a location *)The idea was to prevent an excessive amount of location information. However, all early adopters of this library implemented their own mechanisms to retain the location information, which indicated that the original design was cumbersome in practice.
The new design (partially introduced in 0.1 and then fully implemented in 0.3) is to remember the locations of backtrace frames (the argument loc when calling trace) and use the innermost one as the default location for emit or fatal. An inner backtrace frame, however, will not use the inherited location of another frame to avoid duplicated locations in a backtrace (unless an implementer explicitly specifies the same location). We believe this strikes a good balance between convenience and succinctness. For example,
Reporter.trace ~loc "outer trace with a location" @@ fun () ->
+Reporter.trace "inner trace" @@ fun () ->
+(* the frame ["inner trace"] will not have a location *)
+Reporter.emit Greeting "hello"
+(* the message ["hello"] will have [loc] as its location *)Note: inherited locations can be overwritten by the optional argument loc at any time.
There is a long history of using ASCII printable characters and ANSI escape sequences, and recently also non-ASCII Unicode characters, to draw pictures on terminals. To display compiler diagnostics, this technique has been used to assemble line numbers, code from the end user, code highlighting, and other pieces of information in a visually pleasing way. Non-ASCII Unicode characters (from the implementer or from the end user) greatly expand the vocabulary of ASCII art, and we will call the new art form Unicode art to signify the use of non-ASCII characters.
In asai, we made the unusual choice to abandon column numbers (and any Unicode art that depends on them) so that our Unicode art remains flawless in the presence of tricky Unicode character sequences. In particular, the following highlighting method goes against our design principle:
let foo = f x + ^^^ variable name too ugly
The highlighting assumes that the visual location of foo is at the column 4 (if you count from 0), an assumption that is forbidden to make in asai. The following will explain why a flawless support of Unicode necessarily leads to tossing out the concept of column numbers completely.
Note: "Unicode characters" are not really defined in the Unicode standard, and here they mean Unicode scalar values, that is, all Unicode code points except the surrogate code points (special code points for UTF-16 to represent all scalar values). Although the word "character" has many incompatible meanings and usages, we decided to call scalar values "Unicode characters" anyway because (1) most people are not familiar with the official term "scalar values" and (2) scalar values are the only context-independent unit one can work with in a programming language.
The arrival of non-ASCII Unicode characters imposes new challenges as their visual widths are unpredictable without knowing the exact terminal (or terminal emulator), the exact font, etc. Unicode emoji sequences might be one of the most challenging cases: a pirate flag (🏴☠️) may be shown as a single emoji flag on supported platforms but as a sequence with a black flag (🏴) and a skull (☠️) on other platforms. This means the visual width of the pirate flag is unpredictable. (See Unicode Emoji Section 2.2.) The rainbow flag (🏳️🌈), skin tones, and many other emoji sequences have the same issue. Other less chaotic but still challenging cases include characters whose East Asian width is "Ambiguous". (See UAX #11 for more information about East Asian width.) These challenges bear some similarity with the unpredictability of the visual width of horizontal tabulations, but in a much wilder way.
Due to the unpredictability of visual widths, it is wise to think twice before using emoji sequences or other tricky characters in Unicode art. However, it is difficult to make visually pleasing Unicode art without any assumption. To quantify the degree to which a Unicode art can remain visually pleasing on different platforms, we specify the following four levels of display stability. The levels go from 0 (the most unstable) to 3 (the most stable), where Level 0 (the most unstable) makes the most assumptions, and Level 3 (the most stable) makes almost none. Note that if an implementer decide to integrate content from the end user into their Unicode art, the end user should have the freedom to include arbitrary emoji sequences and tricky characters in their content. The final Unicode art must remain visually pleasing (under the assumptions allowed by the display stability levels) for any user content.
wcwidth and wcswidth). These heuristics are created to help programmers handle more characters, in particular CJK characters, without dramatically changing the code. They however do not solve the core problem (that is, visual width is fundamentally ill-defined) and they often could not handle tricky cases such as emoji sequences. Many compilers are at this level.Level 2b: Stability under only theses assumptions:
Level 2b is the explicit version of Level 2a; we might update the details of Level 2b later to better match our understanding of Level 2a. Collectively, Levels 2a and 2b are called "Level 2". This is where asai is.
Unlike most implementations, which are only at Level 1, our terminal handler strives to achieve Level 2. That means we must not make any assumption about the visual width of the end user's code. The reason is that without (incorrect) strong assumptions about how Unicode characters are rendered, the visual column numbers are ill-defined. On the other hand, Level 3 seems to be too restricted for compiler diagnostics because we cannot show line numbers along with the end user's code. (We cannot assume the numbers "10" and "99" will have the same visual width at Level 3.)
Note: a fixed-width font with enough glyphs that covers many Unicode characters is often technically duospaced, not monospaced, because many CJK characters would occupy a double character visual width. Thus, we do not use the terminology "monospaced".
Proper support of bidirectional text will benefit many potential end users, but unfortunately, we currently do not have the capacity to implement it. The general support of bidirectional text in most system libraries and tools is lacking, and without dedicated effort, it is hard to display bidirectional text properly. This is the area where our current implementation falls short.
On a related note, Unicode Source Code Handling suggests that source code should be segmented into atoms and their display order should remain the same throughout the document to maintain the lexical structure. Each atom should then be displayed via the usual Unicode Bidirectional Algorithm with a few exceptions. Our current implementation cannot follow this advice because it does not know the lexical structure of the end user content.
All positions should be byte-oriented. We believe other popular alternatives proposals are worse:
U+FFFF (such as 😎) will require two code units to form a surrogate pair. Therefore, it is arguably worse than just using Unicode characters. This scheme was unfortunately chosen by the Language Service Protocol (LSP) as the default unit, and until LSP version 3.17 was the only choice. The developers of the protocol made this decision probably because Visual Studio Code was written in JavaScript (and TypeScript), whose strings use UTF-16 encoding. It still takes linear time to count characters from other encodings (such as UTF-8), and the count still does not match the visual perception; even worse, UTF-16 usually takes more space than UTF-8 when ASCII is dominant."asai" is the transliteration of "浅井", the family name of the character Kei Asai (浅井 ケイ) in the Japanese light novel Sagrada Reset (サクラダリセット, also known in English as Sakurada Reset). His ability is perfect photographic memory that is even immune to the "Reset" ability owned by another main character. This OCaml library should record all messages, just like the character.
This tutorial is for an implementer (you!) to adopt this library as quickly as possible. We will assume you are already familiar with OCaml and are using a typical OCaml package structure.
The first step is to create a file Reporter.ml with the following template:
module Message =
+struct
+ (** The type of all messages used in your application. *)
+ type t =
+ | (* ... *)
+ | (* ... *)
+ | (* ... *)
+
+ (** The default severity level of diagnostics with a particular message. *)
+ let default_severity : t -> Asai.Diagnostic.severity =
+ function
+ | (* ... *) -> Bug
+ | (* ... *) -> Error
+ | (* ... *) -> Warning
+
+ (** A short, concise, ideally Google-able string representation for each message. *)
+ let short_code : t -> string =
+ function
+ | (* ... *) -> "E0001"
+ | (* ... *) -> "E0002"
+ | (* ... *) -> "E0003"
+end
+
+(** Include all the goodies from the asai library. *)
+include Asai.Reporter.Make(Message)The most important step is to define the type of messages. It should be a meaningful classification of all the diagnostics you want to send to the end user. For example, UndefinedSymbol could be a reasonable message about failing to find the definition of a symbol. TypeError could be another reasonable message about ill-typed terms. Don't worry about missing details in the message type---you can attach free-form text, location information, and additional remarks to a message. Once you have defined the type of all messages, you will have to define two functions default_severity and short_code:
default_severity: Severity levels describe how serious the end user should take your message (is it an error or a warning?). It seems diagnostics with the same message usually come with the same severity level, so we want you to define a default severity level for each message. You can then save some typing later when sending a diagnostic.short_code: This function is to show a message as short code to the end user. Ideally, the short code should be a Google-able string representation for the end user to find more explanations. Please do not use long descriptions such as "scope-error: undefined symbols" The library will give you plenty of opportunities to add as many details as you want to a message, but not here. The short code should be unambiguous, easily recognizable, and "machine-readable without ChatGPT."Once you have filled out the template, run dune build or other tools to check that everything compiles. If so, you are ready for the next step.
Now, go to the places where you want to send a message to the end user, be it a warning or an error. If you want to print a message and continue the execution, you can emit a string:
Reporter.emit Greeting "hello";
+(* continue doing other things *)where Greeting is the message and "Hello!" is the free-form text that explains the message. The fancier version is emitf, which formats the text like printf and sends it:
Reporter.emitf TypeError "@[<2>this term doesn't look right:@ %a@]" Syntax.pp term;
+(* continue doing other things *)There is an important limitation of emitf though: you should not include any control character (for example the newline character \n) anywhere when using emitf. Use break hints (such as @, and @ ) and boxes instead. See Stdlib.Format for more information on boxes and break hints.
If you wish to terminate your program after sending a message instead of continuing the execution, use fatal instead of emit. There's also a fancier fatalf that works in the same way as emitf.
Now that your program is generating lots of messages, you need a handler to deal with them. The library comes with a stock handler to display those messages in a terminal. Suppose your entry point module looks like this:
let () =
+ (* your application code *)You can use the terminal handler as follows:
module Term = Asai.Tty.Make(Reporter.Message)
+
+let () =
+ Reporter.run ~emit:Term.display ~fatal:(fun d -> Term.display d; exit 1) @@ fun () ->
+ (* your application code *)A handler is actually just a function that takes a diagnostic. Here, any function of type Reporter.Code.t Diagnostic.t -> unit would have worked. We suggest adding exit 1 or something equivalent in the case of fatal to exit the whole program with a non-zero code (as demonstrated in the above snippet); the non-zero exit code will signal other programs that something might have gone wrong.
Great messages come with meaningful backtraces. To add backtraces, you will have to "annotate" your code to generate meaningful stack frames. Suppose this is one of the functions whose invocation should be noted in user-facing backtraces:
let f x y =
+ (* very important code *)Add trace to add a frame to the current backtrace:
let f x y =
+ Reporter.trace "when calling f" @@ fun () ->
+ (* very important code *)Similar to emitf, there is also tracef which allows you to format texts:
let f x y =
+ Reporter.tracef "when calling f on %d and %d" x y @@ fun () ->
+ (* very important code *)We do not recommend adding trace to every single function. Remember they should make sense to the end user!
PS: We have a GitHub issue on spewing debugging information for developers (you!), not the end user. Your comments will help us complete the design.
Good diagnostics also help the end user locate the issues in their program or proof. Here, a location is a range of text from a file or a string. Many functions in your Reporter take an optional location argument loc, including trace, which should be a range highlighting the most relevant part of the text. For example, maybe the term which does not type check should be highlighted. The asai library will take the location information and draw fancy Unicode art on the screen to highlight the text. Here is one snippet showing the usage:
Reporter.emit ~loc Greeting "hello again";
+(* continue doing other things *)You can use Range.make to create such a range manually. However, if you are using ocamllex and Menhir, you certainly want to use provided helper functions. One of them is Range.locate; you can add these lines in your Menhir grammar to generated a node annotated with its location:
%inline
+locate(X):
+ | e = X
+ { Asai.Range.locate_lex $loc e }The annotated node will have type data Range.located where data is the output type of X. Another one is Range.of_lexbuf, which comes in handy when reporting a parsing error:
try Grammar.start Lex.token lexbuf with
+| Lex.SyntaxError token ->
+ Reporter.fatalf ~loc:(Range.of_lexbuf lexbuf) ParsingError
+ "unrecognized token `%s'" (String.escaped token)
+| Grammar.Error ->
+ Reporter.fatal ~loc:(Range.of_lexbuf lexbuf) ParsingError
+ "failed to parse the code"Please take a look at Asai.Range to learn all kinds of ways to create a range!
Note that Reporter will remember and reuse the innermost specified location, and thus you do not have to explicitly pass it. For example, in the following code
Reporter.trace ~loc "when checking this code" @@ fun () ->
+(* ... *)
+Reporter.emit "wow" (* using the location [loc] from above *)
+(* ... *)the inner message "wow" will inherit the location loc from the outer trace function call! You can also use merge_loc to "remember" a location for later use, which is helpful when you want to remember a location but not to leave a trace:
Reporter.merge_loc (Some loc) @@ fun () ->
+(* ... *)
+Reporter.emit "wow" (* using the location [loc] from above *)
+(* ... *)Of course, you can always pass a new location to overwrite the remembered one:
Reporter.merge_loc (Some loc) @@ fun () ->
+(* ... *)
+Reporter.emit ~loc:real_loc "wow" (* using [real_loc] instead *)
+(* ... *)If you have seen an exception from asai like this:
Invalid_argument("Asai.Explicator.explicate: <REASON>; use the debug mode")It means asai has detected invalid ranges. This usually indicates that your lexer or parser is buggy and generates invalid locations. For efficiency, asai by default will not check ranges carefully, but you can force it to do so by using the optional argument debug:
module Term = Asai.Tty.Make(Reporter.Message)
+
+let () =
+ Reporter.run
+ ~emit:(Term.display ~debug:true)
+ ~fatal:(fun d -> Term.display ~debug:true d; exit 1) @@ fun () ->
+ (* your application code *)The checking is very expensive; it is highly recommended to disable the debug mode once you are convinced that your code is correct. At very least, disable it unless the end user explicitly wants to enable it.
Suppose you wanted to use a cool OCaml library which is also using asai (which is probably why it is cool), how should you display the diagnostics from the library as if they are yours? Let's assume the library exposes a module CoolLibrary, and the library authors also followed this tutorial to create a module called CoolLibrary.Reporter. You want to painlessly incorporate the library.
The first step is to extend your message type so that it can embed all messages from the library. Open up your Reporter.ml and update the type and functions as follows.
module Message =
+struct
+ (** The type of all messages used in your application. *)
+ type t =
+ (* ... *)
+ | Cool of CoolLibrary.Reporter.Message.t (** Embedding all messages from [CoolLibrary]. *)
+
+ (** The default severity level of diagnostics with a particular message. *)
+ let default_severity : t -> Asai.Diagnostic.severity =
+ function
+ (* ... *)
+ | Cool _ ->
+ (* You probably should not create new diagnostics using the cool library's messages. *)
+ assert false
+
+ (** A short, concise, ideally Google-able string representation for each message. *)
+ let short_code : t -> string =
+ function
+ (* ... *)
+ | Cool c ->
+ (* You can add a prefix to avoid code collision. *)
+ "C-" ^ CoolLibrary.Reporter.Message.short_code c
+
+ (** It is recommended to add a helper function (such as [cool]) to save typing,
+ and this tutorial will assume you have done that. *)
+ let cool c = Cool c
+endAfter updating the module, move to the end of the Reporter.ml and add the following line:
let lift_cool f = adopt (Asai.Diagnostic.map Message.cool) CoolLibrary.Reporter.run fRemember to run dune build or your development tool to check that everything still compiles. Now you are ready to call any function in the cool library!
PS: If you know Haskell, yes, the name lift was inspired by the monadic lifting from Haskell.
Whenever you want to use the cool library, wrap the code under Reporter.lift_cool---it will take care of backtraces, locations, effects, etc.
Reporter.lift_cool @@ fun () ->
+CoolLibrary.cool_function "argument" 123That's it!
It is tempting to consider wrapping errors (e.g., advocated in Go). However, it seems good backtraces make error wrapping obsolete. To see why one might wish to wrap errors, consider the following code:
Reporter.trace "when loading settings" @@ fun () ->
+let content = Reporter.lift_cool @@ fun () ->
+ CoolLibrary.read "/path/to/some/file.json"
+in
+(* ... *)When the file does not exist, the cool library might output the message that the file does not exist. Together with the trace, the terminal handler will output
￫ error[E123] + ꭍ ￮ when loading settings + ￮ file `/path/to/some/file.json' does not exist
This message is not bad, but suboptimal. There's a disconnection between "settings" and /path/to/some/file.json---how exactly is this file relevant? It is tempting to directly edit the text in the diagnostic to include such information, that is, wrapping the error. However, we suggest improving the trace instead:
let file_path = "/path/to/some/file.json" in
+Reporter.trace "when loading settings from file `%s'" file_path @@ fun () ->
+let content = Reporter.lift_cool @@ fun () ->
+ CoolLibrary.read file_path
+in
+(* ... *)so that the output is
￫ error[E123] + ꭍ ￮ when loading settings from file `/path/to/some/file.json' + ￮ file `/path/to/some/file.json' does not exist
There's no conceptual gap in the message anymore!
If you want to turn everything into an error, add the following lines to the end of your Reporter.ml:
let all_as_errors f = map_diagnostic (fun d -> {d with severity = Error}) fAnd then use Reporter.all_as_errors to turn all diagnostics into errors:
Reporter.all_as_errors @@ fun () -> (* any diagnostic sent here will be an error *)Note that turning a diagnostic into an error does not abort the computation. all_as_errors only makes diagnostics look scarier and it will not affect the control flow. If you instead wish to abort the program the moment any diagnostic is sent, no matter whether it is a warning or an error, do this:
let abort_at_any f = map_diagnostic fatal_diagnostic fWithin abort_at_any, every diagnostic will become fatal:
Reporter.abort_at_any @@ fun () -> (* any diagnostic will abort the program *)Just like the usual try ... with in OCaml, you can use Reporter.try_with to intercept fatal diagnostics. However, unlike diagnostics sent via emit, there is no way to resume the aborted computation (as what you can expect from OCaml exceptions). Therefore, you have to provide a new value as a replacement. For example,
Reporter.try_with ~fatal:(fun _ -> 42) @@ fun () -> Reporter.fatal Abort "abort"will give you the number 42 in the end. It intercepts the fatal diagnostic and gives 42 instead.
We are still expanding this tutorial, but in the meanwhile, you can also check out our 📔 API reference.