diff options
| -rw-r--r-- | dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh | 1 | ||||
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst | 6 | ||||
| -rw-r--r-- | test-suite/output/RecordProjParameter.out | 33 | ||||
| -rw-r--r-- | test-suite/output/RecordProjParameter.v | 21 | ||||
| -rw-r--r-- | vernac/record.ml | 32 |
5 files changed, 88 insertions, 5 deletions
diff --git a/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh new file mode 100644 index 0000000000..9b8d1a63d9 --- /dev/null +++ b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh @@ -0,0 +1 @@ +overlay compcert https://github.com/Lysxia/CompCert no-collision-projection 13852 diff --git a/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst new file mode 100644 index 0000000000..d3ef244cb0 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst @@ -0,0 +1,6 @@ +- **Changed:** + In `Record`, alpha-rename the variable associated with the record to avoid + alpha-renaming parameters of projections + (`#13852 <https://github.com/coq/coq/pull/13852>`_, + fixes `#13727 <https://github.com/coq/coq/issues/13727>`_, + by Li-yao Xia). diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out new file mode 100644 index 0000000000..91ae4b6511 --- /dev/null +++ b/test-suite/output/RecordProjParameter.out @@ -0,0 +1,33 @@ +t1 : Atype -> forall a : Type, a + +t1 is not universe polymorphic +Arguments t1 _ _%type_scope +t1 is transparent +Expands to: Constant RecordProjParameter.t1 +t3 : forall a0 : Atype, t2 a0 + +t3 is not universe polymorphic +t3 is transparent +Expands to: Constant RecordProjParameter.t3 +u1 : Btype -> forall b b0 : Type, b * b0 + +u1 is not universe polymorphic +Arguments u1 _ (_ _)%type_scope +u1 is transparent +Expands to: Constant RecordProjParameter.u1 +u3 : forall b1 : Btype, u2 b1 + +u3 is not universe polymorphic +u3 is transparent +Expands to: Constant RecordProjParameter.u3 +v1 : Ctype -> forall c0 : Type, c0 + +v1 is not universe polymorphic +Arguments v1 _ _%type_scope +v1 is transparent +Expands to: Constant RecordProjParameter.v1 +v3 : forall c : Ctype, v2 c + +v3 is not universe polymorphic +v3 is transparent +Expands to: Constant RecordProjParameter.v3 diff --git a/test-suite/output/RecordProjParameter.v b/test-suite/output/RecordProjParameter.v new file mode 100644 index 0000000000..8b892c694c --- /dev/null +++ b/test-suite/output/RecordProjParameter.v @@ -0,0 +1,21 @@ +Record Atype : Type := + { t1 : forall (a : Type), a + ; t2 : Type + ; t3 : t2 }. +About t1. +About t3. + +Record Btype : Type := + { u1 : forall (b : Type) (b0 : Type), b * b0 + ; u2 : Type + ; u3 : u2 }. +About u1. +About u3. + +Record Ctype : Type := + { v1 : forall (c0 : Type), c0 + ; v2 : Type + ; v3 : v2 + }. +About v1. +About v3. diff --git a/vernac/record.ml b/vernac/record.ml index 96e4a47d2d..ff6bdc5199 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -511,6 +511,32 @@ let inStruc : Recordops.struc_typ -> Libobject.obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) +(** In the type of every projection, the record is bound to a variable named + using the first character of the record type. We rename it to avoid + collisions with names already used in the field types. +*) + +(** Get all names bound at the head of [t]. *) +let rec add_bound_names_constr (names : Id.Set.t) (t : constr) : Id.Set.t = + match destProd t with + | (b, _, t) -> + let names = + match b.binder_name with + | Name.Anonymous -> names + | Name.Name n -> Id.Set.add n names + in add_bound_names_constr names t + | exception DestKO -> names + +(** Get all names bound in any record field. *) +let bound_names_rdata { DataR.fields; _ } : Id.Set.t = + let add_names names field = add_bound_names_constr names (RelDecl.get_type field) in + List.fold_left add_names Id.Set.empty fields + +(** Pick a variable name for a record, avoiding names bound in its fields. *) +let data_name { Data.id; Data.rdata; _ } = + let name = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in + Namegen.next_ident_away name (bound_names_rdata rdata) + (** Main record declaration part: The entry point is [definition_structure], which will match on the @@ -537,11 +563,7 @@ let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls par in let binder_name = match name with - | None -> - let map { Data.id; _ } = - Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) - in - Array.map_of_list map record_data + | None -> Array.map_of_list data_name record_data | Some n -> n in let ntypes = List.length record_data in |