From a1991de2b5aedbccc60a22795500726669fda233 Mon Sep 17 00:00:00 2001 From: favonia Date: Mon, 18 Sep 2023 03:53:58 -0500 Subject: [PATCH 1/3] docs: tweak the docs --- src/DiagnosticData.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/DiagnosticData.ml b/src/DiagnosticData.ml index 0be3340..aa87665 100644 --- a/src/DiagnosticData.ml +++ b/src/DiagnosticData.ml @@ -24,7 +24,7 @@ end (** The type of text. - When we render a diagnostic, the layout engine of the rendering backend should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a message is defined to be a function that takes a formatter and uses it to render the content. Please note that a message itself should not contain literal control characters such as newlines (but break hints such as ["@,"] are okay). *) + When we render a diagnostic, the layout engine of the rendering backend should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a message is defined to be a function that takes a formatter and uses it to render the content. Please note that a message itself should not contain literal control characters (such as newlines) but only break hints (such as [@,]). *) type text = Format.formatter -> unit (** A message is a located text. *) From 097c9202475dc4530f970a995ae323443e443053 Mon Sep 17 00:00:00 2001 From: favonia Date: Mon, 18 Sep 2023 05:57:35 -0500 Subject: [PATCH 2/3] docs: polish more documentation --- src/Diagnostic.mli | 4 ++-- src/DiagnosticData.ml | 5 ++--- src/LoggerSigs.ml | 8 ++++++++ 3 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Diagnostic.mli b/src/Diagnostic.mli index 9794685..5adcca1 100644 --- a/src/Diagnostic.mli +++ b/src/Diagnostic.mli @@ -25,10 +25,10 @@ val kmessagef : (message -> 'b) -> ?loc:Span.t -> ('a, Format.formatter, unit, ' (** {1 Utility Functions} *) -(** A convenience function that turns severities into strings. *) +(** A convenience function that turns a {!type:severity} into a string. *) val string_of_severity : severity -> string -(** A convenience function that turns a message into a string by formatting it with the maximum admissible margin. *) +(** A convenience function that turns a {!type:text} into a string by formatting it with the maximum admissible margin. Note that the resulting string may contain control characters and might not be suitable for constructing another instance of {!type:text} or {!type:message}. *) val string_of_text : text -> string (** A convenience function that maps the message code. This is helpful when using {!val:Logger.S.adopt}. *) diff --git a/src/DiagnosticData.ml b/src/DiagnosticData.ml index aa87665..4eb5154 100644 --- a/src/DiagnosticData.ml +++ b/src/DiagnosticData.ml @@ -24,10 +24,10 @@ end (** The type of text. - When we render a diagnostic, the layout engine of the rendering backend should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a message is defined to be a function that takes a formatter and uses it to render the content. Please note that a message itself should not contain literal control characters (such as newlines) but only break hints (such as [@,]). *) + When we render a diagnostic, the layout engine of the rendering backend 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. The text itself should not contain literal control characters (such as newlines) but only break hints (such as [@,]). Control characters include `0x00-0x1f` (C0 controls), `0x7f` (backspace), and `0x80-0x9f` (C1 controls); in particular, `0x0a` (newline) is a C0 control character. These characters are banned because they would mess up the cursor position. *) type text = Format.formatter -> unit -(** A message is a located text. *) +(** A message is a located {!type:text}. *) type message = text Span.located (** A backtrace is a (backward) list of messages. *) @@ -46,4 +46,3 @@ type 'code t = { additional_messages : message list; (** Additional messages relevant to the main message that are not part of the backtrace. *) } - diff --git a/src/LoggerSigs.ml b/src/LoggerSigs.ml index af5b5b8..b536109 100644 --- a/src/LoggerSigs.ml +++ b/src/LoggerSigs.ml @@ -11,6 +11,8 @@ sig Logger.diagnosticf `TypeError "Term %a does not type check" Syntax.pp tm ]} + Note that the format strings should not contain any control characters. See {!type:Diagnostic.text}. + @param severity The severity (to overwrite the default severity inferred from the message [code]). @param loc The location of the text (usually the code) to highlight. @param backtrace The backtrace (to overwrite the accumulative frames up to this point). @@ -20,6 +22,8 @@ sig (** [kdiagnosticf kont code format ...] is [kont (diagnosticf code format ...)]. + Note that the format strings should not contain any control characters. See {!type:Diagnostic.text}. + @param severity The severity (to overwrite the default severity inferred from the message [code]). @param loc The location of the text (usually the code) to highlight. @param backtrace The backtrace (to overwrite the accumulative frames up to this point). @@ -51,6 +55,8 @@ sig (** [fatalf code format ...] constructs a diagnostic and aborts the current computation with the diagnostic. + Note that the format strings should not contain any control characters. See {!type:Diagnostic.text}. + Example: {[ Logger.fatalf `FileError "Failed to read %s" filepath @@ -83,6 +89,8 @@ sig (** [tracef format ... f] constructs and records a frame, and runs the thunk [f] with the new backtrace. + Note that the format strings should not contain any control characters. See {!type:Diagnostic.text}. + @param loc The location of the text (usually the code) to highlight. *) val tracef : ?loc:Span.t -> ('a, Format.formatter, unit, (unit -> 'b) -> 'b) format4 -> 'a From e206ae8d88bedc5137ee3f067c6069b844d3ac56 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 21 Sep 2023 07:42:46 -0500 Subject: [PATCH 3/3] refactor(Tty): refactor the terminal backend --- src/Utils.ml | 2 + src/tty/Tty.ml | 220 +++++++++++++++++++++++++++++++++++-------------- 2 files changed, 159 insertions(+), 63 deletions(-) diff --git a/src/Utils.ml b/src/Utils.ml index c7e4c7f..9899c4f 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -29,3 +29,5 @@ let group p = | y :: ys -> (acc @> [x]) :: (go[@tailcall]) Emp y ys in go Emp x xs + +let maximum = List.fold_left Int.max Int.min_int diff --git a/src/tty/Tty.ml b/src/tty/Tty.ml index 3d03b35..49c01df 100644 --- a/src/tty/Tty.ml +++ b/src/tty/Tty.ml @@ -16,14 +16,55 @@ module E = Explicator.Make(FileReader)(Style) module Make (Code : Diagnostic.Code) = struct +(* + ๐Ÿญ examples/stlc/source.lambda + โ‡ƒ + 3 โ‡ƒ no, it is not my fault!!! + 4 โ‡ƒ I was just calling some function!!! + โ‡ƒ + [E002] When looking into the meaning of 42 + + ๐Ÿญ examples/stlc/example.lambda + โ”‚ + 1 โ”‚ (check (ฮป รค (ฮป 123 + 2 โ”‚ sdaf)) (โ†’ โ„• (โ†’ โ„• โ„•))) + โ”Š + 20 โ”‚ ahhhhhhhhhhhhhhhhhh + 21 โ”‚ noooooooooooooooooo + โ”ท + [E002] Why am I checking the term (โ†’ โ„• (โ†’ โ„• โ„•)) + which looks amazing!!! + + ๐Ÿญ examples/stlc/example2.lambda + โ”‚ + 3 โ”‚ let x = 1 + 4 โ”‚ let y = 1 + โ”ท + ๐Ÿญ examples/stlc/example3.lambda + โ”‚ + 8 โ”‚ assert (asai is cool) + โ”ท +*) + + (* helper functions *) + let vline attr height str = I.vcat @@ List.init height (fun _ -> I.string attr str) + let column ~align images = let maxby f xs = List.(fold_left max 0 (map f xs)) in let width = maxby I.width images in List.map (I.hsnap ~align width) images |> I.vcat - let attr (severity : Diagnostic.severity) (style : Style.t) = + let hcat_with_pad ~pad l = + I.hcat @@ List.map (I.pad ~l:pad) l + + let vcat_with_pad ~pad l = + I.vcat @@ List.map (I.pad ~b:pad) l + + (* styles *) + + let highlight_style (severity : Diagnostic.severity) (style : Style.t) = let open A in match style with | None -> empty @@ -37,70 +78,122 @@ struct | Error -> fg red | Bug -> bg red ++ fg black - let marked_style = A.st A.underline - let fringe_style = A.fg @@ A.gray 8 - let line_numbers_of_block Explicator.{start_line_num; lines} = - column ~align:`Right @@ - List.map (fun n -> I.string fringe_style @@ Int.to_string n) @@ - List.init (List.length lines) (fun i -> start_line_num + i) - - let display_parts code severity text parts = - if parts = [] then - I.strf "[%s] %t" (Code.to_string code) text - else - let segment Explicator.{style; value = seg} = - I.string (attr severity style) seg - in - let line (segs : _ Explicator.line) = - segs |> List.map segment |> I.hcat - in - let block (b : _ Explicator.block) = - (* We want to display the error message under whatever block contains the highlighted text *) - (b.lines |> List.map line |> I.vcat) <-> - if List.exists (List.exists (function Explicator.{style = (Style.Primary | HighlightedPrimary); _} -> true | _ -> false)) b.lines then - I.pad ~t:1 @@ I.strf "[%s] %t" (Code.to_string code) text - else - I.void 0 0 - in - let part Explicator.{file_path; blocks} = - let line_numbers = blocks |> List.map line_numbers_of_block in - let fringes = line_numbers |> List.map (fun img -> vline fringe_style (I.height img) "โ”‚") in - let line_numbers = line_numbers |> List.map (I.pad ~b:2) |> column ~align:`Right |> I.crop ~b:2 in - let fringe = - I.string fringe_style ("๐Ÿญ") <-> - I.string fringe_style "โ”‚" <-> - (fringes |> List.map (fun img -> img <-> vline fringe_style 2 "โ”Š") |> I.vcat |> I.crop ~b:2) <-> - I.string fringe_style "โ”‚" <-> - I.string fringe_style "โ–ˆ" - in - let side_panel = I.pad ~t:2 ~l:1 ~r:1 line_numbers <|> fringe in - let blocks = blocks |> List.map (fun b -> block b |> I.pad ~b:1) |> I.vcat in - let body = I.pad ~b:1 (I.string A.empty file_path) <-> blocks in - I.pad ~r:1 side_panel <|> body - in - parts |> List.map (fun s -> s |> part |> I.pad ~b:1) |> I.vcat |> I.crop ~b:2 - - let display_message code severity (msg : Diagnostic.message) additional_messages = - let style s x = Explicator.{value = x; style = s} in - let main_span = Option.to_list @@ Option.map (style Style.HighlightedPrimary) msg.loc in - let additional_spans = List.filter_map (fun x -> Option.map (style Style.Additional) x.Span.loc) additional_messages in - let parts = E.explicate ~splitting_threshold:5 (main_span @ additional_spans) in - display_parts code severity msg.value parts - - let display_diagnostic show_backtrace Diagnostic.{code; severity; message; additional_messages; backtrace} = - FileReader.run @@ fun () -> + (* calculating the width of line numbers *) + + let line_number_width explication : int = + let max_line_number_block Explicator.{start_line_num; lines} = + start_line_num + List.length lines - 1 + in + let max_line_number_part Explicator.{blocks; _} = + Utils.maximum @@ List.map max_line_number_block blocks + in + let max_line_number (parts : _ Explicator.explication) = + Utils.maximum @@ List.map max_line_number_part parts + in + String.length @@ Int.to_string @@ max_line_number explication + + (* different parts of the display *) + + (* [ ๐Ÿญ examples/stlc/source.lambda] *) + let render_file_header ~line_number_width ~is_backtrace:_ file_path = + hcat_with_pad ~pad:1 + [ I.void line_number_width 0 + ; I.string fringe_style "๐Ÿญ" + ; I.string A.empty file_path + ] + + (* [ โ‡ƒ ] or [ โ”‚ ] *) + let render_file_header_padding ~line_number_width ~is_backtrace = + hcat_with_pad ~pad:1 + [ I.void line_number_width 0 + ; I.string fringe_style (if is_backtrace then "โ‡ƒ" else "โ”‚") + ] + + let show_code_segment severity Explicator.{style; value = seg} = + I.string (highlight_style severity style) seg + + let show_code_line severity (segs : _ Explicator.line) = + I.hcat @@ List.map (show_code_segment severity) segs + + (* [3 โ‡ƒ no, it is not my fault!!!] *) + let render_block ~line_number_width~is_backtrace ~severity Explicator.{start_line_num; lines} = + List.mapi (fun i line -> + let line_num = start_line_num + i in + hcat_with_pad ~pad:1 + [ I.hsnap ~align:`Right line_number_width (I.string fringe_style (Int.to_string line_num)) + ; I.string fringe_style (if is_backtrace then "โ‡ƒ" else "โ”‚") + ; show_code_line severity line + ] + ) lines + + (* [ โ”Š ] *) + let render_code_block_sep ~line_number_width ~is_backtrace:_ = + hcat_with_pad ~pad:1 + [ I.void line_number_width 0 + ; I.string fringe_style "โ”Š" + ] + + (* [ โ‡ƒ ] or [ โ”ท ] *) + let render_code_part_end ~line_number_width ~is_backtrace = + hcat_with_pad ~pad:1 + [ I.void line_number_width 0 + ; I.string fringe_style (if is_backtrace then "โ‡ƒ" else "โ”ท") + ] + + let render_part ~line_number_width ~is_backtrace ~severity Explicator.{file_path; blocks} = + [ render_file_header ~line_number_width ~is_backtrace file_path + ; render_file_header_padding ~line_number_width ~is_backtrace + ] @ begin - if show_backtrace then - I.pad ~b:1 (I.string A.empty "Backtrace:") <-> - (backtrace |> Bwd.map (fun f -> display_message code severity f [] |> I.pad ~b:1) |> Bwd.to_list |> I.vcat) <-> - I.pad ~b:1 (I.string A.empty "Error:") - else - I.void 0 0 - end + List.concat @@ + List.mapi + (fun i b -> + List.concat + [ if i = 0 then [] else [ render_code_block_sep ~line_number_width ~is_backtrace ] + ; render_block ~line_number_width ~is_backtrace ~severity b + ] + ) blocks + end @ + [ render_code_part_end ~line_number_width ~is_backtrace ] + + let render_explication ~line_number_width ~is_backtrace ~severity parts = + I.vcat @@ List.concat_map (render_part ~line_number_width ~is_backtrace ~severity) parts + + (* message *) + let render_text ~line_number_width:_ ~is_backtrace:_ ~code text = + hcat_with_pad ~pad:1 + [ I.strf "[%s]" (Code.to_string code) + ; I.strf "%t" text + ] + + let render_message ~line_number_width ~is_backtrace ~severity ~code explication text = + render_explication ~line_number_width ~is_backtrace ~severity explication <-> - I.pad ~b:1 (display_message code severity message additional_messages) + render_text ~line_number_width ~is_backtrace ~code text + + let display_message ~is_backtrace ~severity ~code (msg : Diagnostic.message) ~additional_messages = + let explication = + let style s x = Explicator.{value = x; style = s} in + let main_span = Option.to_list @@ Option.map (style Style.HighlightedPrimary) msg.loc in + let additional_spans = List.filter_map (fun x -> Option.map (style Style.Additional) x.Span.loc) additional_messages in + E.explicate ~splitting_threshold:5 (main_span @ additional_spans) + in + let line_number_width = line_number_width explication in + render_message ~line_number_width ~is_backtrace ~severity ~code explication msg.value + + let display_diagnostic show_backtrace Diagnostic.{severity; code; message; backtrace; additional_messages} = + FileReader.run @@ fun () -> + let msgs = + Bwd.snoc + (if show_backtrace then + Bwd.map (display_message ~is_backtrace:true ~severity ~code ~additional_messages:[]) backtrace + else + Emp) + (display_message ~is_backtrace:false ~severity ~code message ~additional_messages) + in + vcat_with_pad ~pad:1 (Bwd.to_list msgs) module F = Explicator.Make(FileReader) @@ -111,8 +204,9 @@ struct let traces = FileReader.run @@ fun () -> Bwd.snoc - (backtrace |> Bwd.map (fun f -> display_message code severity f [])) - (display_message code severity message additional_messages) |> Bwd.to_list |> Array.of_list + (backtrace |> Bwd.map (fun msg -> display_message ~is_backtrace:true ~severity ~code msg ~additional_messages:[])) + (display_message ~is_backtrace:false ~severity ~code message ~additional_messages) + |> Bwd.to_list |> Array.of_list in let len = Array.length traces in let open Notty_unix in