Merge PR coq#19197: Ltac2: add a few APIs about uint63

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

doc/changelog/06-Ltac2-language/19197-ltac2-uint63.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  APIs `compare` `of_int` and `print` in `Ltac2.Uint63`
+  (`#19197 <https://github.com/coq/coq/pull/19197>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -867,6 +867,15 @@ let () =
   Proofview.tclEVARMAP >>= fun sigma ->
   return (Evarutil.has_undefined_evars sigma c)
 
+(** Uint63 *)
+
+let () = define "uint63_compare" (uint63 @-> uint63 @-> ret int) Uint63.compare
+
+let () = define "uint63_of_int" (int @-> ret uint63) Uint63.of_int
+
+let () = define "uint63_print" (uint63 @-> ret pp) @@ fun i ->
+  Pp.str (Uint63.to_string i)
+
 (** Extra equalities *)
 
 let () = define "evar_equal" (evar @-> evar @-> ret bool) Evar.equal

test-suite/ltac2/uint63.v

@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Uint63.
+
+Ltac2 Eval Control.assert_true (equal (of_int 0) (of_int 0)).
+
+Ltac2 Eval Control.assert_false (equal (of_int 0) (of_int 1)).
+
+Ltac2 Eval Control.assert_true (Int.equal (compare (of_int 0) (of_int 42)) -1).
+Ltac2 Eval Control.assert_true (Int.equal (compare (of_int 41) (of_int 41)) 0).
+Ltac2 Eval Control.assert_true (Int.equal (compare (of_int 67) (of_int 43)) 1).
+
+Ltac2 Eval Control.assert_true (String.equal (Message.to_string (print (of_int 567))) "567").

user-contrib/Ltac2/Uint63.v

@@ -13,3 +13,9 @@ Require Import Ltac2.Init.
 Ltac2 Type t := uint63.
 
 Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "uint63_equal".
+
+Ltac2 @external compare : t -> t -> int := "coq-core.plugins.ltac2" "uint63_compare".
+
+Ltac2 @external of_int : int -> t := "coq-core.plugins.ltac2" "uint63_of_int".
+
+Ltac2 @external print : t -> message := "coq-core.plugins.ltac2" "uint63_print".