From 6cd0f09b9ea87f863266ffb1058af3b03ebce41c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 5 Dec 2023 15:57:20 +0100
Subject: [PATCH] Ltac2: Take some small APIs from rewriter (fst/snd, Special
 chars)

---
 user-contrib/Ltac2/Char.v   | 10 ++++++++++
 user-contrib/Ltac2/Init.v   |  5 +++++
 user-contrib/Ltac2/String.v | 11 +++++++++++
 3 files changed, 26 insertions(+)

diff --git a/user-contrib/Ltac2/Char.v b/user-contrib/Ltac2/Char.v
index dd83eb2749428..7cd2f43520e12 100644
--- a/user-contrib/Ltac2/Char.v
+++ b/user-contrib/Ltac2/Char.v
@@ -16,3 +16,13 @@ Ltac2 @external to_int : char -> int := "coq-core.plugins.ltac2" "char_to_int".
 
 Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y).
 Ltac2 compare (x : char) (y : char) : int := Int.compare (to_int x) (to_int y).
+
+(** Special characters *)
+Ltac2 null () : char := Char.of_int 0.
+Ltac2 backspace () : char := Char.of_int 8.
+Ltac2 tab () : char := Char.of_int 9.
+Ltac2 lf () : char := Char.of_int 10.
+Ltac2 newpage () : char := Char.of_int 12.
+Ltac2 cr () : char := Char.of_int 13.
+Ltac2 escape () : char := Char.of_int 27.
+Ltac2 newline () : char := Char.of_int 10.
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 55b4cf65212d7..63632b6ac6bd6 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -41,6 +41,11 @@ Ltac2 Type ('a, 'b, 'c, 'd) format.
 Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
 
+(** Tuples *)
+
+Ltac2 fst (p:'a * 'b) : 'a := let (x,_) := p in x.
+Ltac2 snd (p:'a * 'b) : 'b := let (_,y) := p in y.
+
 (** Pervasive types *)
 
 Ltac2 Type 'a option := [ None | Some ('a) ].
diff --git a/user-contrib/Ltac2/String.v b/user-contrib/Ltac2/String.v
index 14d21d965254d..d4d1a03207036 100644
--- a/user-contrib/Ltac2/String.v
+++ b/user-contrib/Ltac2/String.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Char.
 
 Ltac2 Type t := string.
 
@@ -22,3 +23,13 @@ Ltac2 @external equal : string -> string -> bool := "coq-core.plugins.ltac2" "st
 Ltac2 @external compare : string -> string -> int := "coq-core.plugins.ltac2" "string_compare".
 
 Ltac2 is_empty s := match s with "" => true | _ => false end.
+
+(** Special characters *)
+Ltac2 null () : string := String.make 1 (Char.null ()).
+Ltac2 backspace () : string := String.make 1 (Char.backspace ()).
+Ltac2 tab () : string := String.make 1 (Char.tab ()).
+Ltac2 lf () : string := String.make 1 (Char.lf ()).
+Ltac2 newpage () : string := String.make 1 (Char.newpage ()).
+Ltac2 cr () : string := String.make 1 (Char.cr ()).
+Ltac2 escape () : string := String.make 1 (Char.escape ()).
+Ltac2 newline () : string := String.make 1 (Char.newline ()).