Add Ltac2 Bool.to_string and Message.of_bool/of_list/of_option

doc/changelog/06-Ltac2-language/22241-ltac2-message-printers-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 functions ``Bool.to_string``, ``Message.of_bool``, ``Message.of_list``, ``Message.of_list_with_sep`` and ``Message.of_option``
+  (`#22241 <https://github.com/rocq-prover/rocq/pull/22241>`_,
+  by Jason Gross).

test-suite/ltac2/message_printers.v

@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure.
+Ltac2 check_msg (m : message) (s : string) := check (String.equal (Message.to_string m) s).
+
+Ltac2 Eval check (String.equal (Bool.to_string true) "true").
+Ltac2 Eval check (String.equal (Bool.to_string false) "false").
+Ltac2 Eval check_msg (Message.of_bool true) "true".
+Ltac2 Eval check_msg (Message.of_list Message.of_int [1; 2; 3]) "1; 2; 3".
+Ltac2 Eval check_msg (Message.of_list Message.of_int [1]) "1".
+Ltac2 Eval check_msg (Message.of_list Message.of_int []) "".
+Ltac2 Eval check_msg (Message.of_list_with_sep (Message.of_string ",") Message.of_int [1; 2]) "1,2".
+Ltac2 Eval check_msg (Message.of_option Message.of_int (Some 5)) "Some 5".
+Ltac2 Eval check_msg (Message.of_option Message.of_int None) "None".

theories/Ltac2/Bool.v

@@ -82,3 +82,9 @@ Ltac2 Notation x(self) "||" y(thunk(self)) : 3 :=
   end.
 
 End BoolNotations.
+
+Ltac2 to_string (b : bool) : string :=
+  match b with
+  | true => "true"
+  | false => "false"
+  end.

theories/Ltac2/Message.v

@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Bool.
 
 Ltac2 @ external print : message -> unit := "rocq-runtime.plugins.ltac2" "print".
 
@@ -118,3 +119,28 @@ Ltac2 @ external ikfprintf : ('v -> 'r) -> 'v -> ('a, unit, 'v, 'r) format -> 'a
   "rocq-runtime.plugins.ltac2" "format_ikfprintf".
 
 End Format.
+
+Ltac2 of_bool (b : bool) : message := of_string (Bool.to_string b).
+
+(** [of_list_with_sep sep of_elt l] concatenates the messages
+    [of_elt x] for [x] in [l], separated by [sep]. *)
+Ltac2 of_list_with_sep (sep : message) (of_elt : 'a -> message) (l : 'a list) : message :=
+  let rec aux l :=
+    match l with
+    | [] => empty
+    | [x] => of_elt x
+    | x :: l => concat (of_elt x) (concat sep (aux l))
+    end in
+  aux l.
+
+(** [of_list of_elt l] prints the elements of [l] separated by ["; "]. *)
+Ltac2 of_list (of_elt : 'a -> message) (l : 'a list) : message :=
+  of_list_with_sep (of_string "; ") of_elt l.
+
+(** [of_option of_elt o] prints [Some x] as ["Some "] followed by
+    [of_elt x], and [None] as ["None"]. *)
+Ltac2 of_option (of_elt : 'a -> message) (o : 'a option) : message :=
+  match o with
+  | Some x => concat (of_string "Some ") (of_elt x)
+  | None => of_string "None"
+  end.