feat(Diagnostic): support generalize locations

src/Diagnostic.ml

@@ -2,28 +2,15 @@ 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
   ; backtrace
   ; 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

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} *)
 

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, 'explanation) t = {
   severity : severity;
   (** Severity of the diagnostic. *)
   message : 'message;
   (** The (structured) message. *)
-  explanation : Loctext.t;
+  explanation : 'explanation;
   (** The free-form explanation. *)
-  backtrace : backtrace;
+  backtrace : 'explanation bwd;
   (** The backtrace leading to this diagnostic. *)
-  extra_remarks : Loctext.t 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. *)
 }

src/Explanation.ml

@@ -0,0 +1 @@
+include Explanation_sigs

src/Explanation_sigs.ml

@@ -0,0 +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

src/Location.ml

@@ -0,0 +1 @@
+include Location_sigs

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

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 *)

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]}: