From c427fabcc0a602cdab99d17cfcc53794dca5ce0b Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 31 Oct 2024 09:48:50 -0500 Subject: [PATCH 1/2] wip --- src/Diagnostic_data.ml | 11 ++++------- src/Location.ml | 1 + src/Location_sigs.ml | 9 +++++++++ src/Loctext_sigs.ml | 11 +++++++++++ 4 files changed, 25 insertions(+), 7 deletions(-) create mode 100644 src/Location.ml create mode 100644 src/Location_sigs.ml create mode 100644 src/Loctext_sigs.ml diff --git a/src/Diagnostic_data.ml b/src/Diagnostic_data.ml index 404ddf8..07d2513 100644 --- a/src/Diagnostic_data.ml +++ b/src/Diagnostic_data.ml @@ -8,19 +8,16 @@ type severity = | Error (** A serious error caused by the end user (the user of your proof assistant or compiler) or other external factors (e.g., internet not working). *) | Bug (** A serious error likely caused by a bug in the proof assistant. You would want the end user to report the bug back to you. This is useful for indicating that certain branches in a pattern matching should be "impossible", while printing out debugging information in case the program logic is flawed. *) -(** A backtrace is a (backward) list of loctexts. *) -type backtrace = Loctext.t bwd - (** The type of diagnostics. *) -type 'message t = { +type ('message, 'loctext) t = { severity : severity; (** Severity of the diagnostic. *) message : 'message; (** The (structured) message. *) - explanation : Loctext.t; + explanation : 'loctext; (** The free-form explanation. *) - backtrace : backtrace; + backtrace : 'loctext bwd; (** The backtrace leading to this diagnostic. *) - extra_remarks : Loctext.t bwd; + extra_remarks : 'loctext 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. *) } diff --git a/src/Location.ml b/src/Location.ml new file mode 100644 index 0000000..c193ddd --- /dev/null +++ b/src/Location.ml @@ -0,0 +1 @@ +include Location_sigs diff --git a/src/Location_sigs.ml b/src/Location_sigs.ml new file mode 100644 index 0000000..06f36f1 --- /dev/null +++ b/src/Location_sigs.ml @@ -0,0 +1,9 @@ +(** An auxiliary type to package data with an optional location. *) +type ('data, 'location) located = { value : 'data; loc : 'location option } + +module type S = +sig + type t + val to_range : t -> Range.t option + val pp : Format.formatter -> t -> unit +end diff --git a/src/Loctext_sigs.ml b/src/Loctext_sigs.ml new file mode 100644 index 0000000..238b961 --- /dev/null +++ b/src/Loctext_sigs.ml @@ -0,0 +1,11 @@ + +module type S = +sig + module Location : Location.S + + type t + + val make : ?loc:Location.t -> string -> t + val makef : ?loc:Location.t -> ('a, Format.formatter, unit, t) format4 -> 'a + val kmakef : ?loc:Location.t -> (t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a +end From 00ff7d3b18f5902b5e4c80cc43249c594eea8679 Mon Sep 17 00:00:00 2001 From: favonia Date: Mon, 18 Nov 2024 10:47:16 -0600 Subject: [PATCH 2/2] wip --- src/Diagnostic.ml | 17 +------- src/Diagnostic.mli | 45 +++----------------- src/Diagnostic_data.ml | 8 ++-- src/Explanation.ml | 1 + src/{Loctext_sigs.ml => Explanation_sigs.ml} | 8 +++- src/Loctext.mli | 6 +++ src/Minimum_signatures.ml | 3 ++ 7 files changed, 30 insertions(+), 58 deletions(-) create mode 100644 src/Explanation.ml rename src/{Loctext_sigs.ml => Explanation_sigs.ml} (54%) diff --git a/src/Diagnostic.ml b/src/Diagnostic.ml index c465acb..c07aa29 100644 --- a/src/Diagnostic.ml +++ b/src/Diagnostic.ml @@ -2,7 +2,7 @@ open Bwd include Diagnostic_data -let of_loctext ?(backtrace=Bwd.Emp) ?(extra_remarks=[]) severity message explanation : _ t = +let make ?(backtrace=Bwd.Emp) ?(extra_remarks=[]) severity message explanation : _ t = { severity ; message ; explanation @@ -10,20 +10,7 @@ let of_loctext ?(backtrace=Bwd.Emp) ?(extra_remarks=[]) severity message explana ; extra_remarks = Bwd.of_list extra_remarks } -let of_text ?loc ?backtrace ?extra_remarks severity message text : _ t = - of_loctext ?backtrace ?extra_remarks severity message {loc; value = text} - -let make ?loc ?backtrace ?extra_remarks severity message explanation = - of_text ?loc ?backtrace ?extra_remarks severity message @@ Text.make explanation - -let kmakef ?loc ?backtrace ?extra_remarks k severity message = - Text.kmakef @@ fun text -> - k @@ of_text ?loc ?backtrace ?extra_remarks severity message text - -let makef ?loc ?backtrace ?extra_remarks severity message = - Text.kmakef @@ of_text ?loc ?backtrace ?extra_remarks severity message - -let map f d = {d with message = f d.message} +let map f1 f2 d = {d with message = f1 d.message; explanation = f2 d.explanation} let string_of_text text : string = let buf = Buffer.create 20 in diff --git a/src/Diagnostic.mli b/src/Diagnostic.mli index 55881cc..65f6949 100644 --- a/src/Diagnostic.mli +++ b/src/Diagnostic.mli @@ -1,5 +1,7 @@ (** {1 Types} *) +open Bwd + (* @include *) include module type of Diagnostic_data @@ -17,57 +19,24 @@ include module type of Diagnostic_data @since 0.2.0 *) -val of_text : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> Text.t -> 'message t - -(** [of_loctext severity message loctext] constructs a diagnostic from a {!type:Loctext.t}. - - Example: - {[ - of_loctext Warning ChiError @@ loctext "your Ch'i is critically low" - ]} - - @param backtrace The backtrace (to overwrite the accumulative frames up to this point). - @param extra_remarks Additional remarks that are not part of the backtrace. -*) -val of_loctext : ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> Loctext.t -> 'message t - -(** [make severity message loctext] constructs a diagnostic with the [loctext]. - - Example: - {[ - make Warning ChiError "your Ch'i is critically low" - ]} - - @param backtrace The backtrace (to overwrite the accumulative frames up to this point). - @param extra_remarks Additional remarks that are not part of the backtrace. -*) -val make : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> string -> 'message t +val of_text : ?loc:Range.t -> ?backtrace:'explanation bwd -> ?extra_remarks:'explanation list -> severity -> 'message -> Text.t -> ('message, 'explanation) t -(** [makef severity message format ...] is [of_loctext severity message (Loctext.makef format ...)]. It formats the message and constructs a diagnostic out of it. +(** [of_explanation severity message explanation] constructs a diagnostic from an explanation. Example: {[ - makef Warning ChiError "your %s is critically low" "Ch'i" + of_explanation Warning ChiError @@ Loctext.make "your Ch'i is critically low" ]} - @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). - @param extra_remarks Additional remarks that are not part of the backtrace. -*) -val makef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> ('a, Format.formatter, unit, 'message t) format4 -> 'a - -(** [kmakef kont severity message format ...] is [kont (makef severity message format ...)]. - - @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). @param extra_remarks Additional remarks that are not part of the backtrace. *) -val kmakef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> ('message t -> 'b) -> severity -> 'message -> ('a, Format.formatter, unit, 'b) format4 -> 'a +val make : ?backtrace:'explanation bwd -> ?extra_remarks:'explanation list -> severity -> 'message -> 'explanation -> ('message, 'explanation) t (** {1 Other Helper Functions} *) (** A convenience function that maps the message of a diagnostic. This is helpful when using {!val:Reporter.S.adopt}. *) -val map : ('message1 -> 'message2) -> 'message1 t -> 'message2 t +val map : ('message1 -> 'message2) -> ('explanation1 -> 'explanation2) -> ('message1, 'explanation1) t -> ('message2, 'explanation2) t (** {1 Deprecated Types and Functions} *) diff --git a/src/Diagnostic_data.ml b/src/Diagnostic_data.ml index 07d2513..4f45a0e 100644 --- a/src/Diagnostic_data.ml +++ b/src/Diagnostic_data.ml @@ -9,15 +9,15 @@ type severity = | Bug (** A serious error likely caused by a bug in the proof assistant. You would want the end user to report the bug back to you. This is useful for indicating that certain branches in a pattern matching should be "impossible", while printing out debugging information in case the program logic is flawed. *) (** The type of diagnostics. *) -type ('message, 'loctext) t = { +type ('message, 'explanation) t = { severity : severity; (** Severity of the diagnostic. *) message : 'message; (** The (structured) message. *) - explanation : 'loctext; + explanation : 'explanation; (** The free-form explanation. *) - backtrace : 'loctext bwd; + backtrace : 'explanation bwd; (** The backtrace leading to this diagnostic. *) - extra_remarks : 'loctext bwd; + extra_remarks : 'explanation 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. *) } diff --git a/src/Explanation.ml b/src/Explanation.ml new file mode 100644 index 0000000..783a398 --- /dev/null +++ b/src/Explanation.ml @@ -0,0 +1 @@ +include Explanation_sigs diff --git a/src/Loctext_sigs.ml b/src/Explanation_sigs.ml similarity index 54% rename from src/Loctext_sigs.ml rename to src/Explanation_sigs.ml index 238b961..01ca157 100644 --- a/src/Loctext_sigs.ml +++ b/src/Explanation_sigs.ml @@ -1,11 +1,17 @@ - module type S = sig + (** Location *) module Location : Location.S + (** The type of explanations *) type t + (** Making an explanation from a string *) val make : ?loc:Location.t -> string -> t + + (** Making an explanation by formatting a string *) val makef : ?loc:Location.t -> ('a, Format.formatter, unit, t) format4 -> 'a + + (** Making an explanation by formatting a string, and taking a continuation *) val kmakef : ?loc:Location.t -> (t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a end diff --git a/src/Loctext.mli b/src/Loctext.mli index f684fb6..bc567f0 100644 --- a/src/Loctext.mli +++ b/src/Loctext.mli @@ -1,3 +1,9 @@ +include Explanation + +(** {1 Functors} *) + +module Make (Location : Location.S) : S with Location := Location and type t = Text.t Location.located + (** {1 Types} *) (** A located text *) diff --git a/src/Minimum_signatures.ml b/src/Minimum_signatures.ml index 26a81ca..49b0aa7 100644 --- a/src/Minimum_signatures.ml +++ b/src/Minimum_signatures.ml @@ -29,6 +29,9 @@ sig module Message : Message (** The module for messages. *) + + module Explanation : Explanation + (** The module for explanations. *) val run : ?init_loc:Range.t -> ?init_backtrace:Diagnostic.backtrace -> emit:(Message.t Diagnostic.t -> unit) -> fatal:(Message.t Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a (** [run ~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 {{!val:Asai.Reporter.S.adopt}[adopt]}: