summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-05-28 18:48:56 +0200
committerSon Ho2024-05-28 18:48:56 +0200
commitb5eac0384818e1f51fbfd900ab580514e851b0ca (patch)
tree7fc94f32e32674892154e7e72c2d589470c17f9a
parentae075db15638ee8878bebe3d31affb1aa320e90f (diff)
Fix an issue with some names being ignored when generating unique variable names
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBase.ml40
-rw-r--r--tests/coq/arrays/Arrays.v4
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst4
3 files changed, 23 insertions, 25 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ab7eb50c..815e228f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -351,13 +351,13 @@ let unsafe_names_map_add (id : id) (name : string) (nm : unsafe_names_map) :
[append]: function to append an index to a string
*)
-let basename_to_unique (names_set : StringSet.t)
+let basename_to_unique_aux (collision : string -> bool)
(append : string -> int -> string) (basename : string) : string =
let rec gen (i : int) : string =
let s = append basename i in
- if StringSet.mem s names_set then gen (i + 1) else s
+ if collision s then gen (i + 1) else s
in
- if StringSet.mem basename names_set then gen 1 else basename
+ if collision basename then gen 1 else basename
type names_maps = {
names_map : names_map;
@@ -1841,13 +1841,22 @@ let trait_self_clause_basename = "self_clause"
let name_append_index (basename : string) (i : int) : string =
basename ^ string_of_int i
+let basename_to_unique (ctx : extraction_ctx) (name : string) =
+ let collision s =
+ (* Note that we ignore the "unsafe" names which contain in particular
+ field names: we want to allow using field names for variables if
+ the backend allows such collisions *)
+ StringSet.mem s ctx.names_maps.names_map.names_set
+ || StringSet.mem s ctx.names_maps.strict_names_map.names_set
+ in
+
+ basename_to_unique_aux collision name_append_index name
+
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (span : Meta.span) (basename : string) (id : TypeVarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
let name = ctx_compute_type_var_basename ctx basename in
- let name =
- basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
- in
+ let name = basename_to_unique ctx name in
let ctx = ctx_add span (TypeVarId id) name ctx in
(ctx, name)
@@ -1856,9 +1865,7 @@ let ctx_add_const_generic_var (span : Meta.span) (basename : string)
(id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string
=
let name = ctx_compute_const_generic_var_basename ctx basename in
- let name =
- basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
- in
+ let name = basename_to_unique ctx name in
let ctx = ctx_add span (ConstGenericVarId id) name ctx in
(ctx, name)
@@ -1872,10 +1879,7 @@ let ctx_add_type_vars (span : Meta.span) (vars : (string * TypeVarId.id) list)
(** Generate a unique variable name and add it to the context *)
let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let name =
- basename_to_unique ctx.names_maps.names_map.names_set name_append_index
- basename
- in
+ let name = basename_to_unique ctx basename in
let ctx = ctx_add span (VarId id) name ctx in
(ctx, name)
@@ -1883,20 +1887,14 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
extraction_ctx * string =
let basename = trait_self_clause_basename in
- let name =
- basename_to_unique ctx.names_maps.names_map.names_set name_append_index
- basename
- in
+ let name = basename_to_unique ctx basename in
let ctx = ctx_add span TraitSelfClauseId name ctx in
(ctx, name)
(** Generate a unique trait clause name and add it to the context *)
let ctx_add_local_trait_clause (span : Meta.span) (basename : string)
(id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string =
- let name =
- basename_to_unique ctx.names_maps.names_map.names_set name_append_index
- basename
- in
+ let name = basename_to_unique ctx basename in
let ctx = ctx_add span (LocalTraitClauseId id) name ctx in
(ctx, name)
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 371e4a12..6e4ab188 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -289,9 +289,9 @@ Definition index_all : result u32 :=
let (s1, to_slice_mut_back) := p in
p1 <- index_mut_slice_u32_0 s1;
let (i7, s2) := p1 in
- i8 <- u32_add i6 i7;
+ i9 <- u32_add i6 i7;
_ <- to_slice_mut_back s2;
- Ok i8
+ Ok i9
.
(** [arrays::update_array]:
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 289e603d..26a695bb 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -241,9 +241,9 @@ let index_all : result u32 =
let* (s1, to_slice_mut_back) =
array_to_slice_mut u32 2 (mk_array u32 2 [ 0; 0 ]) in
let* (i7, s2) = index_mut_slice_u32_0 s1 in
- let* i8 = u32_add i6 i7 in
+ let* i9 = u32_add i6 i7 in
let* _ = to_slice_mut_back s2 in
- Ok i8
+ Ok i9
(** [arrays::update_array]:
Source: 'tests/src/arrays.rs', lines 187:0-187:36 *)