Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix quoting and unquoting of primitive strings #1109

Merged
merged 2 commits into from
Oct 30, 2024

Conversation

MathisBD
Copy link

@MathisBD MathisBD commented Oct 29, 2024

This PR fixes the following bug related to quoting primitive strings :

From MetaCoq.Template Require Import All.
From Coq Require Import PrimString.
MetaCoq Test Quote "hello"%pstring.
(* produces (String.String "hello"%pstring) which is ill-typed. *)

The bug comes from the fact that in template-coq's quoting/unquoting code, the ocaml variable named tString is used to refer to two distinct Coq terms :

  • the second constructor of bytestring.string.
  • the primitive string constructor of term.

The fix involves changing the names of a couple ocaml variables : see the diff for more info.

@yforster
Copy link
Member

Could you add a file in the test-suite which checks this behavior? I.e. add the code snippet from the PR as file there?

@yforster
Copy link
Member

Thanks! Once CI goes green I'll squash and merge and cherry-pick the commit over to coq-8.20.

@yforster yforster merged commit 65aa111 into MetaCoq:main Oct 30, 2024
5 checks passed
yforster pushed a commit to yforster/template-coq that referenced this pull request Oct 30, 2024
@MathisBD MathisBD deleted the fix-quote-pstring branch October 30, 2024 14:35
yforster added a commit that referenced this pull request Oct 30, 2024
* initial fix

* update test-suite

Co-authored-by: MathisBD <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants