From f3ca3e97049d122855408068cff00012a324dd96 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Jul 2023 14:04:05 +0200 Subject: [PATCH 1/3] Fixes #17854 anomaly: check for duplicates was too late for disjunctive patterns. --- interp/constrintern.ml | 26 ++++++++------------------ test-suite/output/bug_17854.out | 6 ++++++ test-suite/output/bug_17854.v | 17 +++++++++++++++++ 3 files changed, 31 insertions(+), 18 deletions(-) create mode 100644 test-suite/output/bug_17854.out create mode 100644 test-suite/output/bug_17854.v diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dfe9cc13f311..454dd35438a9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1452,26 +1452,16 @@ let rec adjust_to_down l l' default = | false::l, [] -> default :: adjust_to_down l [] default | false::l, y::l' -> y :: adjust_to_down l l' default -(* @return the first variable that occurs twice in a pattern - -naive n^2 algo *) -let rec has_duplicate = function - | [] -> None - | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l - let loc_of_multiple_pattern pl = Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl)) -let loc_of_lhs lhs = - Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs)) - -let check_linearity lhs ids = - match has_duplicate ids with - | Some id -> - let loc = loc_of_lhs lhs in - Loc.raise ?loc (InternalizationError (NonLinearPattern id)) - | None -> - () +let check_linearity mpl ids = + match List.duplicates (fun id1 id2 -> Id.equal id1.v id2.v) ids with + | id::_ -> + let loc = loc_of_multiple_pattern mpl in + Loc.raise ?loc (InternalizationError (NonLinearPattern id.v)) + | [] -> + () (* Match the number of pattern against the number of matched args *) let check_number_of_pattern loc n l = @@ -2377,6 +2367,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let mpl' = List.map (intern_multiple_pattern env n) mpl in let (idsl,mpl') = List.split mpl' in let ids = List.hd idsl in + List.iter2 check_linearity mpl idsl; check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten mpl') @@ -2385,7 +2376,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) let eqn_ids = List.map (fun x -> x.v) eqn_ids in - check_linearity lhs eqn_ids; let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in diff --git a/test-suite/output/bug_17854.out b/test-suite/output/bug_17854.out new file mode 100644 index 000000000000..fc24045ffd40 --- /dev/null +++ b/test-suite/output/bug_17854.out @@ -0,0 +1,6 @@ +File "./output/bug_17854.v", line 3, characters 11-31: +The command has indeed failed with message: +The variable a is bound several times in pattern. +File "./output/bug_17854.v", line 9, characters 11-31: +The command has indeed failed with message: +The variable a is bound several times in pattern. diff --git a/test-suite/output/bug_17854.v b/test-suite/output/bug_17854.v new file mode 100644 index 000000000000..44fb2bd1ef50 --- /dev/null +++ b/test-suite/output/bug_17854.v @@ -0,0 +1,17 @@ +Fail Check fun b : bool + => match b, b with + | true as a, true as a | true as a, _ => true + | _, _ => false + end. + +Fail Check fun b : bool + => match b, b with + | true as a, true as a => true + | _, _ => false + end. + +Definition f b := + match b, b with + | true as a as a, true as b => true + | _, _ => false + end. From 8b0c27d80914fdb7744562ee81652e671bb1e953 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Jul 2023 14:19:58 +0200 Subject: [PATCH 2/3] Ignore repeated "as id" clauses with same id. --- interp/constrintern.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 454dd35438a9..fb726d43c05f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1624,7 +1624,8 @@ let merge_aliases aliases {loc;v=na} = match na with | Anonymous -> aliases | Name id -> - let alias_ids = aliases.alias_ids @ [make ?loc id] in + let alias_ids = List.add_set (fun id1 id2 -> Id.equal id1.v id2.v) (make ?loc id) aliases.alias_ids in + (* Note: assumes that add_set adds in front, see alias_of *) let alias_map = match aliases.alias_ids with | [] -> aliases.alias_map | {v=id'} :: _ -> Id.Map.add id id' aliases.alias_map @@ -1633,7 +1634,7 @@ let merge_aliases aliases {loc;v=na} = let alias_of als = match als.alias_ids with | [] -> Anonymous - | {v=id} :: _ -> Name id + | l -> Name (List.last l).v (** {6 Expanding notations } From 391fbcf2af6e07fec4852a0cc7cb2a009e4ca4ed Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Jul 2023 14:15:21 +0200 Subject: [PATCH 3/3] Adding changelog for #17857 --- ...ix17854-too-late-duplicate-var-check-pattern-matching.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/02-specification-language/17857-master+fix17854-too-late-duplicate-var-check-pattern-matching.rst diff --git a/doc/changelog/02-specification-language/17857-master+fix17854-too-late-duplicate-var-check-pattern-matching.rst b/doc/changelog/02-specification-language/17857-master+fix17854-too-late-duplicate-var-check-pattern-matching.rst new file mode 100644 index 000000000000..61c8e4aada7a --- /dev/null +++ b/doc/changelog/02-specification-language/17857-master+fix17854-too-late-duplicate-var-check-pattern-matching.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Anomaly in the presence of duplicate variables within a disjunctive pattern + (`#17857 `_, + fixes `#17854 `_, + by Hugo Herbelin).