From 76a6808a5a7471a440a9ec8fb6124fd184d039e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Aug 2024 13:20:00 +0200
Subject: [PATCH] Add `ident_to_string`, based on code by @lepigre.
---
iris/proofmode/string_ident.v | 36 ++++++++++++++++++++++++++++++++++-
1 file changed, 35 insertions(+), 1 deletion(-)
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 25f6992de..de2c57765 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -74,10 +74,44 @@ Module StringToIdent.
Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
End StringToIdent.
+Module IdentToString.
+ Import Ltac2.
+
+ Ltac2 char_to_coq_byte (c : char) : constr :=
+ let (ind, inst) :=
+ match Constr.Unsafe.kind constr:(byte) with
+ | Constr.Unsafe.Ind ind inst => (ind, inst)
+ | _ => Control.zero (Invalid_argument None)
+ end
+ in
+ let c := Constr.Unsafe.constructor ind (Char.to_int c) in
+ Constr.Unsafe.make (Constr.Unsafe.Constructor c inst).
+
+ Ltac2 string_to_coq_string (s : string) : constr :=
+ let len := String.length s in
+ let rec to_string acc i :=
+ if Int.equal i -1 then acc else
+ let c := String.get s i in
+ let byte := char_to_coq_byte c in
+ let a := compute constr:(Ascii.ascii_of_byte $byte) in
+ to_string constr:(String $a $acc) (Int.sub i 1)
+ in
+ to_string constr:(EmptyString) (Int.sub len 1).
+
+ Ltac2 ident_to_string (id : ident) : constr :=
+ string_to_coq_string (Ident.to_string id).
+
+ Ltac ident_to_string_cps :=
+ ltac2:(id r |- let id := Option.get (Ltac1.to_ident id) in
+ let s := ident_to_string id in
+ Ltac1.apply r [Ltac1.of_constr s] Ltac1.run).
+End IdentToString.
+
(** Finally we wrap everything up intro a tactic that renames a variable given
by ident [id] into the name given by string [s]. *)
Ltac rename_by_string id s :=
StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
-(* We also directly expose the CPS primitive. *)
+(* We also directly expose the CPS primitives. *)
Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
+Ltac ident_to_string_cps := IdentToString.ident_to_string_cps.
--
GitLab