From 300157fc6176856f3f792d956925af366ef3329e Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 19 Aug 2020 08:13:08 -0700 Subject: Do not refresh the names of implicit arguments. Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`. --- .../12756-jashug-dont-refresh-argument-names.sh | 9 +++++++ .../12756-dont-refresh-argument-names.rst | 9 +++++++ interp/impargs.ml | 30 ++++++++-------------- test-suite/bugs/closed/bug_12001.v | 24 +++++++++++++++++ test-suite/output/Arguments_renaming.out | 2 -- test-suite/output/Arguments_renaming.v | 1 - test-suite/output/Implicit.out | 2 +- test-suite/success/Typeclasses.v | 2 +- vernac/comArguments.ml | 8 ------ 9 files changed, 54 insertions(+), 33 deletions(-) create mode 100644 dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh create mode 100644 doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst create mode 100644 test-suite/bugs/closed/bug_12001.v diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh new file mode 100644 index 0000000000..54fdd87566 --- /dev/null +++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then + + mathcomp_CI_REF=dont-refresh-argument-names-overlay + mathcomp_CI_GITURL=https://github.com/jashug/math-comp + + oddorder_CI_REF=dont-refresh-argument-names-overlay + oddorder_CI_GITURL=https://github.com/jashug/odd-order + +fi diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst new file mode 100644 index 0000000000..b0cf4ca4e3 --- /dev/null +++ b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tweaked the algorithm giving default names to arguments. + Should reduce the frequency that argument names get an + unexpected suffix. + Also makes :flag:`Mangle Names` not mess up argument names. + (`#12756 `_, + fixes `#12001 `_ + and `#6785 `_, + by Jasper Hugunin). diff --git a/interp/impargs.ml b/interp/impargs.ml index db102470b0..48961c6c8a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -20,7 +20,6 @@ open Lib open Libobject open EConstr open Reductionops -open Namegen open Constrexpr module NamedDecl = Context.Named.Declaration @@ -247,24 +246,15 @@ let is_rigid env sigma t = is_rigid_head sigma t | _ -> true -let find_displayed_name_in sigma all avoid na (env, b) = - let envnames_b = (env, b) in - let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in sigma flag avoid na b - else compute_displayed_name_in sigma flag avoid na b - -let compute_implicits_names_gen all env sigma t = +let compute_implicits_names env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid names t = + let rec aux env names t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in - aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b | _ -> List.rev names - in aux env Id.Set.empty [] t - -let compute_implicits_names = compute_implicits_names_gen true + in aux env [] t let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in @@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t = (f.strict || f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual env sigma t -let compute_implicits_flags env sigma f all t = +let compute_implicits_flags env sigma f t = List.combine - (compute_implicits_names_gen all env sigma t) + (compute_implicits_names env sigma t) (compute_implicits_explanation_flags env sigma f t) let compute_auto_implicits env sigma flags enriching t = @@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) = let rec prepare_implicits i f = function | [] -> [] - | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") - | (Name id, Some imp)::imps -> + | (na, Some imp)::imps -> let imps' = prepare_implicits (i+1) f imps in - Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps' + let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in + Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits (i+1) f imps let set_manual_implicits silent flags enriching autoimps l = @@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l = let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] - else let l = compute_implicits_flags env sigma f false t in + else let l = compute_implicits_flags env sigma f t in [DefaultImpArgs, prepare_implicits 1 f l] (*s Constants. *) diff --git a/test-suite/bugs/closed/bug_12001.v b/test-suite/bugs/closed/bug_12001.v new file mode 100644 index 0000000000..19533e49f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_12001.v @@ -0,0 +1,24 @@ +(* Argument names don't get mangled *) +Set Mangle Names. +Lemma leibniz_equiv_iff {A : Type} (x y : A) : True. +Proof. tauto. Qed. +Check leibniz_equiv_iff (A := nat) 2 3 : True. +Unset Mangle Names. + +(* Coq doesn't make up names for arguments *) +Definition bar (a a : nat) : nat := 3. +Arguments bar _ _ : assert. +Fail Arguments bar a a0 : assert. + +(* This definition caused an anomaly in a version of this PR +without the change to prepare_implicits *) +Set Implicit Arguments. +Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I. +Fail Check foo (H := 2). + +Definition baz (a b : nat) := b. +Arguments baz a {b}. +Set Mangle Names. +Definition baz2 (a b : nat) := b. +Arguments baz2 a {b}. +Unset Mangle Names. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e0aa758812..c28bb14eb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -84,8 +84,6 @@ Argument lists should agree on the names they provide. The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Some argument names are duplicated: F -The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6ac09cf771..6001850046 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,7 +48,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. -Fail Arguments eq_refl {F F}, [F] F : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index ef7667936c..2265028d3e 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x0]%nat_scope +Arguments d2 [x x]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 563651cfa5..7acaa92b89 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Arguments unit {m m0 α}. +Arguments unit {m _ α}. Arguments Monad : clear implicits. Notation "'return' t" := (unit t). diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 360e228bfc..be9cc059a7 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -213,14 +213,6 @@ let vernac_arguments ~section_local reference args more_implicits flags = in CErrors.user_err ~hdr:"vernac_declare_arguments" msg end; - let duplicate_names = - List.duplicates Name.equal (List.filter ((!=) Anonymous) names) - in - if not (List.is_empty duplicate_names) then begin - CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++ - prlist_with_sep pr_comma Name.print duplicate_names) - end; - let implicits = List.map (fun { name; implicit_status = i } -> (name,i)) args in -- cgit v1.2.3