Fix quoting and unquoting of primitive strings (MetaCoq#1109)

* initial fix

* update test-suite

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

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

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"

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 *)

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).
+