From 3cbf404737281de4adc6cd543b43ff2879587f74 Mon Sep 17 00:00:00 2001
From: MathisBD <75327344+MathisBD@users.noreply.github.com>
Date: Wed, 30 Oct 2024 15:04:15 +0100
Subject: [PATCH] Fix quoting and unquoting of primitive strings (#1109)

* initial fix

* update test-suite
---
 template-coq/src/constr_denoter.ml     | 4 ++--
 template-coq/src/constr_quoter.ml      | 4 ++--
 template-coq/src/constr_reification.ml | 8 ++++----
 template-coq/theories/Constants.v      | 1 +
 test-suite/bug_quote_pstring.v         | 8 ++++++++
 5 files changed, 17 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bug_quote_pstring.v

diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
index c0cbc21e4..56167a949 100644
--- a/template-coq/src/constr_denoter.ml
+++ b/template-coq/src/constr_denoter.ml
@@ -93,9 +93,9 @@ struct
   let unquote_string trm =
     let rec go n trm =
       let (h,args) = app_full trm [] in
-      if constr_equall h tEmptyString then
+      if constr_equall h tBsEmptyString then
         Bytes.create n
-      else if constr_equall h tString then
+      else if constr_equall h tBsString then
         match args with
           c :: s :: [] ->
           let res = go (n + 1) s in
diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml
index fff2a8d20..aab8d1d31 100644
--- a/template-coq/src/constr_quoter.ml
+++ b/template-coq/src/constr_quoter.ml
@@ -156,10 +156,10 @@ struct
     let rec go from acc =
       if from < 0 then acc
       else
-        let term = constr_mkApp (tString, [| quote_char (String.get s from) ; acc |]) in
+        let term = constr_mkApp (tBsString, [| quote_char (String.get s from) ; acc |]) in
         go (from - 1) term
     in
-    go (len - 1) (Lazy.force tEmptyString)
+    go (len - 1) (Lazy.force tBsEmptyString)
 
   let quote_string s =
     try Hashtbl.find string_hash s
diff --git a/template-coq/src/constr_reification.ml b/template-coq/src/constr_reification.ml
index c590bb610..d56ead567 100644
--- a/template-coq/src/constr_reification.ml
+++ b/template-coq/src/constr_reification.ml
@@ -67,8 +67,8 @@ struct
   let template s = resolve ("metacoq.template." ^ s)
   let template_ref s = resolve_ref ("metacoq.template." ^ s)
 
-  let tString = resolve "metacoq.string.cons"
-  let tEmptyString = resolve "metacoq.string.nil"
+  let tBsString = resolve "metacoq.string.cons"
+  let tBsEmptyString = resolve "metacoq.string.nil"
   let tO = resolve "metacoq.nat.zero"
   let tS = resolve "metacoq.nat.succ"
   let tnat = resolve "metacoq.nat.type"
@@ -151,12 +151,12 @@ struct
   let tmk_branch = ast "mk_branch"
   let tmkdecl = ast "mkdecl"
   let (tTerm,tRel,tVar,tEvar,tSort,tCast,tProd,
-       tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj,tInt,tFloat,tArray) =
+       tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj,tInt,tFloat,tString,tArray) =
     (ast "term", ast "tRel", ast "tVar", ast "tEvar",
      ast "tSort", ast "tCast", ast "tProd", ast "tLambda",
      ast "tLetIn", ast "tApp", ast "tCase", ast "tFix",
      ast "tConstruct", ast "tConst", ast "tInd", ast "tCoFix", ast "tProj", ast "tInt", ast "tFloat",
-     ast "tArray")
+     ast "tString", ast "tArray")
   let tkername = ast "kername"
   let tmodpath = ast "modpath"
   let tMPfile = ast "MPfile"
diff --git a/template-coq/theories/Constants.v b/template-coq/theories/Constants.v
index 62c1a06a7..3a2f6770a 100644
--- a/template-coq/theories/Constants.v
+++ b/template-coq/theories/Constants.v
@@ -178,6 +178,7 @@ Register MetaCoq.Template.Ast.tFix as metacoq.ast.tFix.
 Register MetaCoq.Template.Ast.tCoFix as metacoq.ast.tCoFix.
 Register MetaCoq.Template.Ast.tInt as metacoq.ast.tInt.
 Register MetaCoq.Template.Ast.tFloat as metacoq.ast.tFloat.
+Register MetaCoq.Template.Ast.tString as metacoq.ast.tString.
 Register MetaCoq.Template.Ast.tArray as metacoq.ast.tArray.
 
 (* Local and global declarations *)
diff --git a/test-suite/bug_quote_pstring.v b/test-suite/bug_quote_pstring.v
new file mode 100644
index 000000000..2142d4d2d
--- /dev/null
+++ b/test-suite/bug_quote_pstring.v
@@ -0,0 +1,8 @@
+(* See PR #1109. *)
+
+From MetaCoq.Template Require Import All.
+From Coq Require Import PrimString.
+
+MetaCoq Quote Definition quote_test := "quote_me"%pstring.
+MetaCoq Unquote Definition unquote_test := (tString "unquote_me"%pstring).
+