Merge pull request #841 from hacspec/fix-839-fstar-string-name-clash

fix(engine/fstar): add `string` to the list of protected names
hacspec · Aug 13, 2024 · 35faf49 · 35faf49
2 parents 46df005 + 4b1e8f7
commit 35faf49
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 6 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -78,7 +78,7 @@ module FStarNamePolicy = struct
 
   let index_field_transform index = "_" ^ index
 
-  let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and"]
+  let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"]
 end
 
 module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (FStarNamePolicy)

diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap
@@ -20,10 +20,12 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-
-[stdout]
-diagnostics = []
+exit = 1
+[[stdout.diagnostics]]
+message = '''
+(Coq backend) something is not implemented yet.
+[ty] node str'''
+spans = ['Span { lo: Loc { line: 160, col: 0 }, hi: Loc { line: 160, col: 43 }, filename: Real(LocalPath("naming/src/lib.rs")), rust_span_data: None }']
 
 [stdout.files]
 "Naming.v" = '''
@@ -92,6 +94,8 @@ Definition ff__g__impl_1__g (self : t_Foo_t) : uint_size :=
 Definition reserved_names (val : int8) (noeq : int8) (of : int8) : int8 :=
   (val.+noeq).+of.
 
+(*item error backend*)
+
 Record t_Arity1 (T : _) : Type := {
   0 : T;
 }.

diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -139,6 +139,9 @@ let ff__g__impl_1__g (self: t_Foo) : usize = sz 1
 
 let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of
 
+/// From issue https://github.com/hacspec/hax/issues/839
+let string_shadows (v_string n: string) : Prims.unit = ()
+
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]

diff --git a/tests/naming/Cargo.toml b/tests/naming/Cargo.toml
@@ -6,4 +6,4 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.hax-tests]
-into."fstar+coq" = { snapshot = "stdout" }
+into."fstar" = { snapshot = "stdout" }
diff --git a/tests/naming/src/lib.rs b/tests/naming/src/lib.rs
@@ -155,3 +155,6 @@ mod ambiguous_names {
         debug(0, a)
     }
 }
+
+/// From issue https://github.com/hacspec/hax/issues/839
+fn string_shadows(string: &str, n: &str) {}