Make extract matches return warnings

a.txt

@@ -0,0 +1,118 @@
+use indexmap::IndexSet;
+
+use super::type_check::{DefinitionTypes, Type};
+use crate::term::{Adt, Book, MatchNum, Name, Pattern, Rule};
+use std::collections::BTreeMap;
+
+impl Book {
+  /// For each pattern-matching definition, check that any given value will match at least one of the rules.
+  /// We assume that all patterns have been type checked already.
+  pub fn check_exhaustive_patterns(&self, def_types: &DefinitionTypes) -> Result<(), String> {
+    for (def_id, def) in &self.defs {
+      let def_name = self.def_names.name(def_id).unwrap();
+      let types = &def_types[def_id];
+      let rules_to_check = Vec::from_iter(0 .. def.rules.len());
+      check_pattern(&mut vec![], &self.adts, &def.rules, types, rules_to_check, def_name)?;
+    }
+    Ok(())
+  }
+}
+
+fn check_pattern(
+  match_path: &mut Vec<Name>,
+  adts: &BTreeMap<Name, Adt>,
+  rules: &[Rule],
+  types: &[Type],
+  rules_to_check: Vec<usize>,
+  def_name: &Name,
+) -> Result<(), String> {
+  let mut vars = IndexSet::new();
+  if let Some(pat_type) = types.first() {
+    // For each constructor of the pattern, which rules match with it.
+    // If no rules match a given constructor, the pattern is non-exhaustive.
+    let rules_matching_ctrs = match pat_type {
+      // We can skip non pattern matching arguments
+      Type::Any => BTreeMap::from([(Name::new("_"), rules_to_check)]),
+      Type::Adt(adt_nam) => {
+        let adt = &adts[adt_nam];
+        // Find which rules match each constructor
+        let mut next_rules_to_check: BTreeMap<Name, Vec<usize>> =
+          BTreeMap::from_iter(adt.ctrs.keys().cloned().map(|ctr| (ctr, vec![])));
+        for rule_idx in rules_to_check {
+          let pat = &rules[rule_idx].pats[match_path.len()];
+          match pat {
+            // Rules with a var pattern are relevant to all constructors.
+            Pattern::Var(v) => {
+              vars.insert(v.clone());
+              next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx))
+            }
+            Pattern::Ctr(ctr_nam, _) => next_rules_to_check.get_mut(ctr_nam).unwrap().push(rule_idx),
+            // We already type checked, so no other patterns will appear here.
+            _ => unreachable!(),
+          }
+        }
+        next_rules_to_check
+      }
+      Type::Tup => BTreeMap::from([(Name::new("(_,_)"), rules_to_check)]),
+      Type::Num => {
+        let mut next_rules_to_check: BTreeMap<Name, Vec<usize>> =
+          BTreeMap::from([(Name::new("0"), vec![]), (Name::new("+"), vec![])]);
+        for rule_idx in rules_to_check {
+          let pat = &rules[rule_idx].pats[match_path.len()];
+          match pat {
+            Pattern::Var(_) => next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx)),
+            Pattern::Num(MatchNum::Zero) => {
+              next_rules_to_check.get_mut(&Name::new("0")).unwrap().push(rule_idx);
+            }
+            Pattern::Num(MatchNum::Succ { .. }) => {
+              next_rules_to_check.get_mut(&Name::new("+")).unwrap().push(rule_idx);
+            }
+            _ => unreachable!(),
+          }
+        }
+        next_rules_to_check
+      }
+    };
+
+    // Check that each constructor matches at least one rule and then check the next pattern recursively.
+    for (ctr, matching_rules) in rules_matching_ctrs {
+      if matching_rules.is_empty() {
+        let missing = get_missing_pattern(match_path, ctr, &types[1 ..], adts);
+        return Err(format!(
+          "Non-exhaustive pattern at definition '{}'. Hint: ({} {}) not covered.",
+          def_name, def_name, missing
+        ));
+      } else {
+        println!("{matching_rules:?}");
+        let mut match_path = match_path.to_vec();
+        match_path.push(ctr);
+        check_pattern(&mut match_path, adts, rules, &types[1 ..], matching_rules, def_name)?;
+      }
+    }
+  }
+  Ok(())
+}
+
+/// Returns a string with the first pattern not covered by the definition.
+fn get_missing_pattern(
+  match_path: &[Name],
+  missing_ctr: Name,
+  remaining_types: &[Type],
+  adts: &BTreeMap<Name, Adt>,
+) -> String {
+  let mut missing_set: Vec<_> = match_path.iter().map(|x| x.to_string()).collect();
+  missing_set.push(missing_ctr.to_string());
+  for typ in remaining_types {
+    missing_set.push(first_ctr_of_type(typ, adts));
+  }
+  missing_set.join(" ")
+}
+
+fn first_ctr_of_type(typ: &Type, adts: &BTreeMap<Name, Adt>) -> String {
+  match typ {
+    Type::Any => "_".to_string(),
+    Type::Tup => "(_,_)".to_string(),
+    Type::Num => "0".to_string(),
+    Type::Adt(adt_name) => adts[adt_name].ctrs.keys().next().unwrap().to_string(),
+  }
+}

main.hvm

@@ -0,0 +1,11 @@
+data Bool = True | False
+
+data L = (C x xs) | (N)
+
+main =
+  match N {
+  | *: 1
+  | *: 2
+  }
+
+// main = (Foo True False)

src/lib.rs

@@ -10,7 +10,7 @@ use std::time::Instant;
 use term::{
   book_to_nets, net_to_term,
   term_to_net::{HvmcNames, Labels},
-  Book, DefId, DefNames, ReadbackError, Term,
+  Book, DefId, DefNames, Name, ReadbackError, Term,
 };
 
 pub mod hvmc_net;
@@ -26,24 +26,25 @@ pub fn check_book(mut book: Book) -> Result<(), String> {
 }
 
 pub fn compile_book(book: &mut Book, opt_level: OptimizationLevel) -> Result<CompileResult, String> {
-  let main = desugar_book(book, opt_level)?;
+  let (main, warnings) = desugar_book(book, opt_level)?;
   let (nets, hvmc_names, labels) = book_to_nets(book, main);
   let mut core_book = nets_to_hvmc(nets, &hvmc_names)?;
   pre_reduce_book(&mut core_book, opt_level >= OptimizationLevel::Heavy)?;
   if opt_level >= OptimizationLevel::Heavy {
     prune_defs(&mut core_book);
   }
-  Ok(CompileResult { core_book, hvmc_names, labels, warnings: vec![] })
+  Ok(CompileResult { core_book, hvmc_names, labels, warnings })
 }
 
-pub fn desugar_book(book: &mut Book, opt_level: OptimizationLevel) -> Result<DefId, String> {
+pub fn desugar_book(book: &mut Book, opt_level: OptimizationLevel) -> Result<(DefId, Vec<Warning>), String> {
+  let mut warnings = Vec::new();
   let main = book.check_has_main()?;
   book.check_shared_names()?;
   book.encode_strs()?;
   book.encode_lists()?;
   book.generate_scott_adts();
   book.resolve_refs()?;
-  encode_pattern_matching(book)?;
+  encode_pattern_matching(book, &mut warnings)?;
   book.normalize_native_matches()?;
   book.check_unbound_vars()?;
   book.make_var_names_unique();
@@ -57,15 +58,15 @@ pub fn desugar_book(book: &mut Book, opt_level: OptimizationLevel) -> Result<Def
   if opt_level >= OptimizationLevel::Heavy {
     book.prune(main);
   }
-  Ok(main)
+  Ok((main, warnings))
 }
 
-pub fn encode_pattern_matching(book: &mut Book) -> Result<(), String> {
+pub fn encode_pattern_matching(book: &mut Book, warnings: &mut Vec<Warning>) -> Result<(), String> {
   book.resolve_ctrs_in_pats();
   book.check_unbound_pats()?;
   book.desugar_let_destructors();
   book.desugar_implicit_match_binds();
-  book.extract_adt_matches()?;
+  book.extract_adt_matches(warnings)?;
   book.flatten_rules();
   let def_types = book.infer_def_types()?;
   book.check_exhaustive_patterns(&def_types)?;
@@ -177,11 +178,17 @@ impl std::fmt::Debug for CompileResult {
   }
 }
 
-pub enum Warning {}
+pub enum Warning {
+  MatchOnlyVars { def_name: Name },
+}
 
 impl std::fmt::Display for Warning {
-  fn fmt(&self, _: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-    match *self {}
+  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    match self {
+      Warning::MatchOnlyVars { def_name } => {
+        write!(f, "Match expression at definition '{def_name}' only uses var patterns.")
+      }
+    }
   }
 }
 

src/term/transform/desugar_match_expressions.rs

@@ -1,5 +1,9 @@
-use crate::term::{
-  display::DisplayJoin, Book, DefId, DefNames, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, Type,
+use crate::{
+  term::{
+    display::DisplayJoin, Book, DefId, DefNames, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term,
+    Type,
+  },
+  Warning,
 };
 use indexmap::IndexSet;
 use itertools::Itertools;
@@ -8,12 +12,15 @@ use std::collections::{BTreeMap, HashMap, HashSet};
 impl Book {
   /// Extracts adt match terms into pattern matching functions.
   /// Creates rules with potentially nested patterns, so the flattening pass needs to be called after.
-  pub fn extract_adt_matches(&mut self) -> Result<(), String> {
+  pub fn extract_adt_matches(&mut self, warnings: &mut Vec<Warning>) -> Result<(), String> {
     let book = &mut MatchesBook::new(&mut self.def_names);
     for (def_id, def) in &mut self.defs {
       let def_name = book.def_names.name(def_id).cloned().unwrap();
       for rule in def.rules.iter_mut() {
-        rule.body.extract_adt_matches(&def_name, &self.ctrs, book, &mut 0).map_err(|err| err.to_string())?;
+        rule
+          .body
+          .extract_adt_matches(&def_name, &self.ctrs, book, &mut 0, warnings)
+          .map_err(|err| err.to_string())?;
       }
     }
     self.defs.append(&mut book.new_defs);
@@ -92,11 +99,16 @@ impl Term {
     ctrs: &HashMap<Name, Name>,
     book: &mut MatchesBook,
     match_count: &mut usize,
+    warnings: &mut Vec<Warning>,
   ) -> Result<(), MatchError> {
     match self {
       Term::Match { scrutinee: box Term::Var { .. }, arms } => {
+        let all_vars = arms.iter().all(|(pat, ..)| matches!(pat, Pattern::Var(..)));
+        if all_vars && arms.len() > 1 {
+          warnings.push(crate::Warning::MatchOnlyVars { def_name: def_name.clone() });
+        }
         for (_, term) in arms.iter_mut() {
-          term.extract_adt_matches(def_name, ctrs, book, match_count)?;
+          term.extract_adt_matches(def_name, ctrs, book, match_count, warnings)?;
         }
         let matched_type = infer_match_type(arms.iter().map(|(x, _)| x), ctrs)?;
         match matched_type {
@@ -116,7 +128,7 @@ impl Term {
       }
 
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
-        bod.extract_adt_matches(def_name, ctrs, book, match_count)?;
+        bod.extract_adt_matches(def_name, ctrs, book, match_count, warnings)?;
       }
       Term::App { fun: fst, arg: snd, .. }
       | Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
@@ -124,8 +136,8 @@ impl Term {
       | Term::Tup { fst, snd }
       | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. } => {
-        fst.extract_adt_matches(def_name, ctrs, book, match_count)?;
-        snd.extract_adt_matches(def_name, ctrs, book, match_count)?;
+        fst.extract_adt_matches(def_name, ctrs, book, match_count, warnings)?;
+        snd.extract_adt_matches(def_name, ctrs, book, match_count, warnings)?;
       }
       Term::Var { .. }
       | Term::Lnk { .. }

tests/golden_tests.rs

@@ -148,7 +148,7 @@ fn flatten_rules() {
     book.desugar_let_destructors();
     book.desugar_implicit_match_binds();
     book.check_unbound_pats()?;
-    book.extract_adt_matches()?;
+    book.extract_adt_matches(&mut vec![])?;
     book.flatten_rules();
     Ok(book.to_string())
   })
@@ -171,7 +171,7 @@ fn encode_pattern_match() {
     book.encode_lists()?;
     book.generate_scott_adts();
     book.resolve_refs()?;
-    encode_pattern_matching(&mut book)?;
+    encode_pattern_matching(&mut book, &mut vec![])?;
     Ok(book.to_string())
   })
 }

tests/golden_tests/run_file/match_vars.hvm

@@ -0,0 +1,5 @@
+main=
+  match 0 {
+  | true: 1
+  | false: 0
+  }

tests/snapshots/run_file__match_vars.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/match_vars.hvm
+---
+Could not run the code because of the previous warnings