From fb21101ff77715d034dd3dadee8afb7199a57f41 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 22 Oct 2024 12:38:26 +0000 Subject: [PATCH] Add warning for unreachable pattern matching rules (#737) --- CHANGELOG.md | 9 +- src/fun/transform/desugar_match_defs.rs | 84 +++++++++++++++---- tests/golden_tests.rs | 6 +- .../simplify_matches__adt_tup_era.bend.snap | 4 + .../simplify_matches__already_flat.bend.snap | 6 ++ ...plify_matches__double_unwrap_box.bend.snap | 4 + ...mplify_matches__irrefutable_case.bend.snap | 22 +++++ .../simplify_matches__nested.bend.snap | 5 ++ ...lify_matches__redundant_with_era.bend.snap | 5 ++ 9 files changed, 127 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0b84da7f..771cd93f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,8 +7,12 @@ and this project does not currently adhere to a particular versioning scheme. ## [Unreleased] +### Added + +- Emit a warning when a rule in a pattern matching function is unreachable. ([#736][gh-736]) + ### Fixed -- Fix type checker not properly unifying all the arms of a match expression. +- Fix type checker not properly unifying all the arms of a match expression. ([#734][gh-734]) ## [0.2.37] - 2024-10-18 @@ -379,6 +383,7 @@ and this project does not currently adhere to a particular versioning scheme. [0.2.35]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.35 [0.2.36]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.36 [0.2.37]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.37 +[Unreleased]: https://github.com/HigherOrderCO/Bend/compare/0.2.37...HEAD [gh-424]: https://github.com/HigherOrderCO/Bend/issues/424 [gh-427]: https://github.com/HigherOrderCO/Bend/issues/427 [gh-443]: https://github.com/HigherOrderCO/Bend/issues/443 @@ -436,3 +441,5 @@ and this project does not currently adhere to a particular versioning scheme. [gh-674]: https://github.com/HigherOrderCO/Bend/issues/674 [gh-675]: https://github.com/HigherOrderCO/Bend/issues/675 [gh-706]: https://github.com/HigherOrderCO/Bend/issues/706 +[gh-734]: https://github.com/HigherOrderCO/Bend/issues/734 +[gh-736]: https://github.com/HigherOrderCO/Bend/issues/736 diff --git a/src/fun/transform/desugar_match_defs.rs b/src/fun/transform/desugar_match_defs.rs index 39bbb0c9..da2a06ff 100644 --- a/src/fun/transform/desugar_match_defs.rs +++ b/src/fun/transform/desugar_match_defs.rs @@ -3,6 +3,7 @@ use crate::{ fun::{builtins, Adts, Constructors, Ctx, Definition, FanKind, Name, Num, Pattern, Rule, Tag, Term}, maybe_grow, }; +use itertools::Itertools; use std::collections::{BTreeSet, HashSet}; pub enum DesugarMatchDefErr { @@ -10,6 +11,7 @@ pub enum DesugarMatchDefErr { NumMissingDefault, TypeMismatch { expected: Type, found: Type, pat: Pattern }, RepeatedBind { bind: Name }, + UnreachableRule { idx: usize, nam: Name, pats: Vec }, } impl Ctx<'_> { @@ -30,6 +32,12 @@ impl Ctx<'_> { def_name.clone(), def.source.clone(), ), + DesugarMatchDefErr::UnreachableRule { .. } => self.info.add_function_warning( + err, + WarningType::UnreachableMatch, + def_name.clone(), + def.source.clone(), + ), } } } @@ -49,10 +57,22 @@ impl Definition { let args = (0..self.arity()).map(|i| Name::new(format!("%arg{i}"))).collect::>(); let rules = std::mem::take(&mut self.rules); - match simplify_rule_match(args.clone(), rules, vec![], ctrs, adts) { + let idx = (0..rules.len()).collect::>(); + let mut used = BTreeSet::new(); + match simplify_rule_match(args.clone(), rules.clone(), idx.clone(), vec![], &mut used, ctrs, adts) { Ok(body) => { let body = Term::rfold_lams(body, args.into_iter().map(Some)); self.rules = vec![Rule { pats: vec![], body }]; + for i in idx { + if !used.contains(&i) { + let e = DesugarMatchDefErr::UnreachableRule { + idx: i, + nam: self.name.clone(), + pats: rules[i].pats.clone(), + }; + errs.push(e); + } + } } Err(e) => errs.push(e), } @@ -123,24 +143,32 @@ fn fix_repeated_binds(rules: &mut [Rule]) -> Vec { /// expression, together with the remaining match arguments. /// /// Linearizes all the arguments that are used in at least one of the bodies. +/// +/// `args`: Name of the generated argument variables that sill have to be processed. +/// `rules`: The rules to simplify. +/// `idx`: The original index of the rules, to check for unreachable rules. +/// `with`: Name of the variables to be inserted in the `with` clauses. fn simplify_rule_match( args: Vec, rules: Vec, + idx: Vec, with: Vec, + used: &mut BTreeSet, ctrs: &Constructors, adts: &Adts, ) -> Result { if args.is_empty() { + used.insert(idx[0]); Ok(rules.into_iter().next().unwrap().body) } else if rules[0].pats.iter().all(|p| p.is_wildcard()) { - Ok(irrefutable_fst_row_rule(args, rules.into_iter().next().unwrap())) + Ok(irrefutable_fst_row_rule(args, rules.into_iter().next().unwrap(), idx[0], used)) } else { let typ = Type::infer_from_def_arg(&rules, 0, ctrs)?; match typ { - Type::Any => var_rule(args, rules, with, ctrs, adts), - Type::Fan(fan, tag, tup_len) => fan_rule(args, rules, with, fan, tag, tup_len, ctrs, adts), - Type::Num => num_rule(args, rules, with, ctrs, adts), - Type::Adt(adt_name) => switch_rule(args, rules, with, adt_name, ctrs, adts), + Type::Any => var_rule(args, rules, idx, with, used, ctrs, adts), + Type::Fan(fan, tag, tup_len) => fan_rule(args, rules, idx, with, used, fan, tag, tup_len, ctrs, adts), + Type::Num => num_rule(args, rules, idx, with, used, ctrs, adts), + Type::Adt(adt_name) => switch_rule(args, rules, idx, with, adt_name, used, ctrs, adts), } } } @@ -148,7 +176,7 @@ fn simplify_rule_match( /// Irrefutable first row rule. /// Short-circuits the encoding in case the first rule always matches. /// This is useful to avoid unnecessary pattern matching. -fn irrefutable_fst_row_rule(args: Vec, rule: Rule) -> Term { +fn irrefutable_fst_row_rule(args: Vec, rule: Rule, idx: usize, used: &mut BTreeSet) -> Term { let mut term = rule.body; for (arg, pat) in args.into_iter().zip(rule.pats.into_iter()) { match pat { @@ -166,6 +194,7 @@ fn irrefutable_fst_row_rule(args: Vec, rule: Rule) -> Term { _ => unreachable!(), } } + used.insert(idx); term } @@ -176,7 +205,9 @@ fn irrefutable_fst_row_rule(args: Vec, rule: Rule) -> Term { fn var_rule( mut args: Vec, rules: Vec, + idx: Vec, mut with: Vec, + used: &mut BTreeSet, ctrs: &Constructors, adts: &Adts, ) -> Result { @@ -202,7 +233,7 @@ fn var_rule( with.push(arg); - simplify_rule_match(new_args, new_rules, with, ctrs, adts) + simplify_rule_match(new_args, new_rules, idx, with, used, ctrs, adts) } /// Tuple rule. @@ -224,7 +255,9 @@ fn var_rule( fn fan_rule( mut args: Vec, rules: Vec, + idx: Vec, with: Vec, + used: &mut BTreeSet, fan: FanKind, tag: Tag, len: usize, @@ -263,7 +296,7 @@ fn fan_rule( let bnd = new_args.clone().map(|x| Pattern::Var(Some(x))).collect(); let args = new_args.chain(old_args).collect(); - let nxt = simplify_rule_match(args, new_rules, with, ctrs, adts)?; + let nxt = simplify_rule_match(args, new_rules, idx, with, used, ctrs, adts)?; let term = Term::Let { pat: Box::new(Pattern::Fan(fan, tag.clone(), bnd)), val: Box::new(Term::Var { nam: arg }), @@ -276,7 +309,9 @@ fn fan_rule( fn num_rule( mut args: Vec, rules: Vec, + idx: Vec, with: Vec, + used: &mut BTreeSet, ctrs: &Constructors, adts: &Adts, ) -> Result { @@ -303,12 +338,14 @@ fn num_rule( let mut num_bodies = vec![]; for num in nums.iter() { let mut new_rules = vec![]; - for rule in rules.iter() { + let mut new_idx = vec![]; + for (rule, &idx) in rules.iter().zip(&idx) { match &rule.pats[0] { Pattern::Num(n) if n == num => { let body = rule.body.clone(); let rule = Rule { pats: rule.pats[1..].to_vec(), body }; new_rules.push(rule); + new_idx.push(idx); } Pattern::Var(var) => { let mut body = rule.body.clone(); @@ -321,17 +358,19 @@ fn num_rule( } let rule = Rule { pats: rule.pats[1..].to_vec(), body }; new_rules.push(rule); + new_idx.push(idx); } _ => (), } } - let body = simplify_rule_match(args.clone(), new_rules, with.clone(), ctrs, adts)?; + let body = simplify_rule_match(args.clone(), new_rules, new_idx, with.clone(), used, ctrs, adts)?; num_bodies.push(body); } // Default case let mut new_rules = vec![]; - for rule in rules { + let mut new_idx = vec![]; + for (rule, &idx) in rules.into_iter().zip(&idx) { if let Pattern::Var(var) = &rule.pats[0] { let mut body = rule.body.clone(); if let Some(var) = var { @@ -343,11 +382,12 @@ fn num_rule( } let rule = Rule { pats: rule.pats[1..].to_vec(), body }; new_rules.push(rule); + new_idx.push(idx); } } let mut default_with = with.clone(); default_with.push(pred_var.clone()); - let default_body = simplify_rule_match(args.clone(), new_rules, default_with, ctrs, adts)?; + let default_body = simplify_rule_match(args.clone(), new_rules, new_idx, default_with, used, ctrs, adts)?; // Linearize previously matched vars and current args. let with = with.into_iter().chain(args).collect::>(); @@ -446,11 +486,14 @@ fn fast_pred_access(body: &mut Term, cur_num: u32, var: &Name, pred_var: &Name) /// } /// ``` /// Where `case` represents a call of the [`simplify_rule_match`] function. +#[allow(clippy::too_many_arguments)] fn switch_rule( mut args: Vec, rules: Vec, + idx: Vec, with: Vec, adt_name: Name, + used: &mut BTreeSet, ctrs: &Constructors, adts: &Adts, ) -> Result { @@ -463,7 +506,8 @@ fn switch_rule( let args = new_args.clone().chain(old_args.clone()).collect(); let mut new_rules = vec![]; - for rule in &rules { + let mut new_idx = vec![]; + for (rule, &idx) in rules.iter().zip(&idx) { let old_pats = rule.pats[1..].to_vec(); match &rule.pats[0] { // Same ctr, extract subpatterns. @@ -475,6 +519,7 @@ fn switch_rule( let body = rule.body.clone(); let rule = Rule { pats, body }; new_rules.push(rule); + new_idx.push(idx); } // Var, match and rebuild the constructor. // var pat1 ... patN: body @@ -493,6 +538,7 @@ fn switch_rule( } let rule = Rule { pats, body }; new_rules.push(rule); + new_idx.push(idx); } _ => (), } @@ -502,7 +548,7 @@ fn switch_rule( return Err(DesugarMatchDefErr::AdtNotExhaustive { adt: adt_name, ctr: ctr_nam.clone() }); } - let body = simplify_rule_match(args, new_rules, with.clone(), ctrs, adts)?; + let body = simplify_rule_match(args, new_rules, new_idx, with.clone(), used, ctrs, adts)?; new_arms.push((Some(ctr_nam.clone()), new_args.map(Some).collect(), body)); } @@ -606,6 +652,14 @@ impl std::fmt::Display for DesugarMatchDefErr { DesugarMatchDefErr::RepeatedBind { bind } => { write!(f, "Repeated bind in pattern matching rule: '{bind}'.") } + DesugarMatchDefErr::UnreachableRule { idx, nam, pats } => { + write!( + f, + "Unreachable pattern matching rule '({}{})' (rule index {idx}).", + nam, + pats.iter().map(|p| format!(" {p}")).join("") + ) + } } } } diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index cf6cd3a2..52bd8edd 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -245,7 +245,9 @@ fn readback_hvm() { fn simplify_matches() { run_golden_test_dir(function_name!(), &|code, path| { let diagnostics_cfg = DiagnosticsConfig { - irrefutable_match: Severity::Allow, + unused_definition: Severity::Allow, + irrefutable_match: Severity::Warning, + unreachable_match: Severity::Warning, ..DiagnosticsConfig::new(Severity::Error, true) }; let mut book = parse_book_single_file(code, path)?; @@ -275,7 +277,7 @@ fn simplify_matches() { ctx.book.make_var_names_unique(); ctx.prune(false); - Ok(ctx.book.to_string()) + Ok(format!("{}\n{}", ctx.book, ctx.info)) }) } diff --git a/tests/snapshots/simplify_matches__adt_tup_era.bend.snap b/tests/snapshots/simplify_matches__adt_tup_era.bend.snap index 8666664b..7e4403f6 100644 --- a/tests/snapshots/simplify_matches__adt_tup_era.bend.snap +++ b/tests/snapshots/simplify_matches__adt_tup_era.bend.snap @@ -13,3 +13,7 @@ Tuple/Pair/tag: _ Tuple/Pair: (Any -> Any -> Tuple) (Tuple/Pair) = λa λb λc (c Tuple/Pair/tag a b) +Warnings: +In tests/golden_tests/simplify_matches/adt_tup_era.bend : +In definition 'Foo': + Unreachable pattern matching rule '(Foo *)' (rule index 1). diff --git a/tests/snapshots/simplify_matches__already_flat.bend.snap b/tests/snapshots/simplify_matches__already_flat.bend.snap index c6e0ba5c..a1ded270 100644 --- a/tests/snapshots/simplify_matches__already_flat.bend.snap +++ b/tests/snapshots/simplify_matches__already_flat.bend.snap @@ -73,3 +73,9 @@ Baz/CtrB3/tag: _ Baz/CtrB3: (Any -> Baz) (Baz/CtrB3) = λa λb (b Baz/CtrB3/tag a) +Warnings: +In tests/golden_tests/simplify_matches/already_flat.bend : +In definition 'Rule4': + Unreachable pattern matching rule '(Rule4 x)' (rule index 2). +In definition 'Rule6': + Unreachable pattern matching rule '(Rule6 b)' (rule index 1). diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap b/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap index d3856a5f..1b20fe30 100644 --- a/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap +++ b/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap @@ -13,3 +13,7 @@ Boxed/Box/tag: _ Boxed/Box: (Any -> Boxed) (Boxed/Box) = λa λb (b Boxed/Box/tag a) +Warnings: +In tests/golden_tests/simplify_matches/double_unwrap_box.bend : +In definition 'DoubleUnbox': + Unreachable pattern matching rule '(DoubleUnbox * x)' (rule index 1). diff --git a/tests/snapshots/simplify_matches__irrefutable_case.bend.snap b/tests/snapshots/simplify_matches__irrefutable_case.bend.snap index 455013a7..8e1f5e2a 100644 --- a/tests/snapshots/simplify_matches__irrefutable_case.bend.snap +++ b/tests/snapshots/simplify_matches__irrefutable_case.bend.snap @@ -22,3 +22,25 @@ unchecked v5: Any unchecked main: Any (main) = (v1, v2, v3, v4, v5) +Warnings: +In tests/golden_tests/simplify_matches/irrefutable_case.bend : +In definition 'v1': + Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored. + Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition. + If this is not a mistake, consider using a 'let' expression instead. +In definition 'v2': + Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored. + Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition. + If this is not a mistake, consider using a 'let' expression instead. +In definition 'v3': + Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored. + Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition. + If this is not a mistake, consider using a 'let' expression instead. +In definition 'v4': + Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored. + Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition. + If this is not a mistake, consider using a 'let' expression instead. +In definition 'v5': + Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored. + Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition. + If this is not a mistake, consider using a 'let' expression instead. diff --git a/tests/snapshots/simplify_matches__nested.bend.snap b/tests/snapshots/simplify_matches__nested.bend.snap index 36a661f7..7ad3c9c1 100644 --- a/tests/snapshots/simplify_matches__nested.bend.snap +++ b/tests/snapshots/simplify_matches__nested.bend.snap @@ -34,3 +34,8 @@ Baz/CtrC/tag: _ Baz/CtrC: Baz (Baz/CtrC) = λa (a Baz/CtrC/tag) +Warnings: +In tests/golden_tests/simplify_matches/nested.bend : +In definition 'Rule': + Unreachable pattern matching rule '(Rule (Foo/CtrA a b))' (rule index 2). + Unreachable pattern matching rule '(Rule x)' (rule index 4). diff --git a/tests/snapshots/simplify_matches__redundant_with_era.bend.snap b/tests/snapshots/simplify_matches__redundant_with_era.bend.snap index 75981be8..5690bd9c 100644 --- a/tests/snapshots/simplify_matches__redundant_with_era.bend.snap +++ b/tests/snapshots/simplify_matches__redundant_with_era.bend.snap @@ -7,3 +7,8 @@ unchecked Fn2: Any unchecked main: Any (main) = * +Warnings: +In tests/golden_tests/simplify_matches/redundant_with_era.bend : +In definition 'Fn2': + Unreachable pattern matching rule '(Fn2 0 *)' (rule index 1). + Unreachable pattern matching rule '(Fn2 a *)' (rule index 2).