frontend: Invoke new exhaustivness check through annotation

dinfuehr · Dec 8, 2024 · 0d18f5e · 0d18f5e
1 parent deaf07e
commit 0d18f5e
Show file tree

Hide file tree

Showing 7 changed files with 141 additions and 25 deletions.
diff --git a/dora-frontend/src/exhaustiveness.rs b/dora-frontend/src/exhaustiveness.rs
@@ -1,3 +1,5 @@
+use std::collections::HashSet;
+
 use dora_parser::ast;
 use dora_parser::ast::visit::{self, Visitor};
 use fixedbitset::FixedBitSet;
@@ -12,6 +14,7 @@ pub fn check(sa: &Sema) {
                 sa,
                 file_id: fct.file_id,
                 analysis: fct.analysis(),
+                is_new_exhaustiveness: fct.is_new_exhaustiveness,
             };
             visit::walk_fct(&mut visitor, &fct.ast);
         }
@@ -22,13 +25,14 @@ struct Exhaustiveness<'a> {
     sa: &'a Sema,
     analysis: &'a AnalysisData,
     file_id: SourceFileId,
+    is_new_exhaustiveness: bool,
 }
 
 impl<'a> Visitor for Exhaustiveness<'a> {
     fn visit_expr(&mut self, e: &ast::ExprData) {
         match *e {
             ast::ExprData::Match(ref expr) => {
-                if self.sa.flags.new_exhaustiveness {
+                if self.is_new_exhaustiveness {
                     // Improved exhaustiveness check is WIP and not enabled by default.
                     check_match2(self.sa, self.analysis, self.file_id, expr);
                 } else {
@@ -176,7 +180,7 @@ fn check_match2(
 
     let missing_patterns = check_exhaustive(matrix, 1);
 
-    if missing_patterns.is_empty() {
+    if !missing_patterns.is_empty() {
         sa.report(
             file_id,
             node.expr.span(),
@@ -217,7 +221,29 @@ fn check_exhaustive(matrix: Vec<Vec<Pattern>>, n: usize) -> Vec<Vec<Pattern>> {
             result
         }
 
-        Signature::Complete => unimplemented!(),
+        Signature::Complete => {
+            let ctors = discover_constructors(&matrix);
+            let arity = 0;
+            let ctors_count = 2;
+
+            if ctors.len() == ctors_count {
+                let mut combined_result = Vec::new();
+
+                for id in 0..ctors.len() {
+                    let new_matrix = matrix
+                        .iter()
+                        .flat_map(|r| specialize_row_for_constructor(r, id, arity))
+                        .collect::<Vec<_>>();
+
+                    let mut result = check_exhaustive(new_matrix, n - 1);
+                    combined_result.append(&mut result);
+                }
+
+                combined_result
+            } else {
+                unimplemented!()
+            }
+        }
     }
 }
 
@@ -231,24 +257,91 @@ fn discover_signature(matrix: &[Vec<Pattern>]) -> Signature {
 
     match row.last().expect("missing pattern") {
         Pattern::Alt(..) => unimplemented!(),
-        Pattern::Literal(_) => unimplemented!(),
+        Pattern::Literal(value) => match value {
+            LiteralValue::Bool(..) => Signature::Complete,
+            LiteralValue::Char(..)
+            | LiteralValue::Float(..)
+            | LiteralValue::Int(..)
+            | LiteralValue::String(..) => Signature::Incomplete,
+        },
         Pattern::Any => Signature::Incomplete,
         Pattern::Ctor(..) => Signature::Complete,
         Pattern::Tuple(..) => Signature::Complete,
     }
 }
 
+fn discover_constructors(matrix: &[Vec<Pattern>]) -> HashSet<usize> {
+    let mut constructors = HashSet::new();
+
+    for row in matrix {
+        match row.last().expect("missing pattern") {
+            Pattern::Alt(..) => unimplemented!(),
+            Pattern::Literal(value) => match value {
+                LiteralValue::Bool(value) => {
+                    constructors.insert(*value as usize);
+                }
+                _ => unimplemented!(),
+            },
+            Pattern::Any => unimplemented!(),
+            Pattern::Ctor(..) => unimplemented!(),
+            Pattern::Tuple(..) => unimplemented!(),
+        }
+    }
+
+    constructors
+}
+
 fn check_useful(_matrix: &[Vec<Pattern>], _new_pattern: &[Pattern]) -> bool {
     true
 }
 
 fn specialize_row_for_any(row: &[Pattern]) -> Option<Vec<Pattern>> {
     let last = row.last().expect("missing pattern");
-    if last.is_any() {
-        let count = row.len();
-        Some(row[0..count - 1].to_vec())
-    } else {
-        None
+
+    match last {
+        Pattern::Alt(..) => unimplemented!(),
+        Pattern::Literal(..) | Pattern::Ctor(..) => None,
+        Pattern::Any => {
+            let count = row.len();
+            Some(row[0..count - 1].to_vec())
+        }
+        Pattern::Tuple(..) => unimplemented!(),
+    }
+}
+
+fn specialize_row_for_constructor(
+    row: &[Pattern],
+    id: usize,
+    arity: usize,
+) -> Option<Vec<Pattern>> {
+    let last = row.last().expect("missing pattern");
+
+    match last {
+        Pattern::Alt(..) => unimplemented!(),
+        Pattern::Literal(value) => match value {
+            LiteralValue::Bool(value) => {
+                assert_eq!(arity, 0);
+                if id == *value as usize {
+                    Some(row[0..row.len() - 1].to_vec())
+                } else {
+                    None
+                }
+            }
+
+            _ => unimplemented!(),
+        },
+        Pattern::Ctor(ctor_id, params) => {
+            assert_eq!(arity, params.len());
+            if id == *ctor_id {
+                let mut result = row[0..row.len() - 1].to_vec();
+                result.extend_from_slice(params);
+                Some(result)
+            } else {
+                None
+            }
+        }
+        Pattern::Any => unimplemented!(),
+        Pattern::Tuple(..) => unimplemented!(),
     }
 }
 
@@ -272,15 +365,6 @@ enum Pattern {
     Alt(Vec<Pattern>),
 }
 
-impl Pattern {
-    fn is_any(&self) -> bool {
-        match self {
-            Pattern::Any => true,
-            _ => false,
-        }
-    }
-}
-
 fn convert_pattern(sa: &Sema, analysis: &AnalysisData, pattern: &ast::Pattern) -> Pattern {
     match pattern {
         ast::Pattern::Underscore(..) => Pattern::Any,
@@ -372,7 +456,7 @@ fn convert_pattern(sa: &Sema, analysis: &AnalysisData, pattern: &ast::Pattern) -
 
 #[cfg(test)]
 mod tests {
-    use crate::tests::err;
+    use crate::tests::{err, ok};
     use crate::ErrorMessage;
 
     #[test]
@@ -446,4 +530,31 @@ mod tests {
             ErrorMessage::MatchUnreachablePattern,
         );
     }
+
+    #[test]
+    fn exhaustive_bool() {
+        ok("
+            @NewExhaustiveness
+            fn f(v: Bool) {
+                match v {
+                    true => {}
+                    false => {}
+                }
+            }
+        ");
+    }
+
+    #[test]
+    fn exhaustive_int() {
+        ok("
+            @NewExhaustiveness
+            fn f(v: Int) {
+                match v {
+                    1 => {}
+                    2 => {}
+                    _ => {}
+                }
+            }
+        ");
+    }
 }
diff --git a/dora-frontend/src/program_parser.rs b/dora-frontend/src/program_parser.rs
@@ -706,6 +706,7 @@ impl<'x> visit::Visitor for TopLevelDeclaration<'x> {
                 Annotation::Pub,
                 Annotation::ForceInline,
                 Annotation::NeverInline,
+                Annotation::NewExhaustiveness,
             ],
         );
 
@@ -1296,6 +1297,7 @@ pub struct ParsedModifierList {
     pub is_internal: bool,
     pub is_force_inline: bool,
     pub is_never_inline: bool,
+    pub is_new_exhaustiveness: bool,
 }
 
 impl ParsedModifierList {
@@ -1318,6 +1320,7 @@ enum Annotation {
     ForceInline,
     NeverInline,
     Error,
+    NewExhaustiveness,
 }
 
 impl Annotation {
@@ -1334,6 +1337,7 @@ impl Annotation {
             Annotation::OptimizeImmediately => "Optimize",
             Annotation::ForceInline => "ForceInline",
             Annotation::NeverInline => "NeverInline",
+            Annotation::NewExhaustiveness => "NewExhaustiveness",
             Annotation::Error => "<error>",
         }
     }
@@ -1416,6 +1420,11 @@ fn check_modifier(
                     Annotation::NeverInline
                 }
 
+                "NewExhaustiveness" => {
+                    parsed_modifiers.is_new_exhaustiveness = true;
+                    Annotation::NewExhaustiveness
+                }
+
                 _ => {
                     sa.report(
                         file_id,

diff --git a/dora-frontend/src/sema.rs b/dora-frontend/src/sema.rs
@@ -90,7 +90,6 @@ pub struct SemaFlags {
     pub packages: Vec<(String, FileContent)>,
     pub program_file: Option<FileContent>,
     pub boots: bool,
-    pub new_exhaustiveness: bool,
 }
 
 impl SemaFlags {
@@ -104,7 +103,6 @@ impl SemaFlags {
             packages,
             program_file: Some(FileContent::Content(input.to_string())),
             boots: false,
-            new_exhaustiveness: false,
         }
     }
 
@@ -118,7 +116,6 @@ impl SemaFlags {
             packages,
             program_file: Some(FileContent::Content(input.to_string())),
             boots: false,
-            new_exhaustiveness: true,
         }
     }
 }

diff --git a/dora-frontend/src/sema/functions.rs b/dora-frontend/src/sema/functions.rs
@@ -37,6 +37,7 @@ pub struct FctDefinition {
     pub is_internal: bool,
     pub is_force_inline: bool,
     pub is_never_inline: bool,
+    pub is_new_exhaustiveness: bool,
     pub params: Params,
     pub return_type: ParsedType,
 
@@ -85,6 +86,7 @@ impl FctDefinition {
             is_internal: modifiers.is_internal,
             is_force_inline: modifiers.is_force_inline,
             is_never_inline: modifiers.is_never_inline,
+            is_new_exhaustiveness: modifiers.is_new_exhaustiveness,
             analysis: OnceCell::new(),
             type_param_definition: type_params,
             container_type_params: OnceCell::new(),

diff --git a/dora-language-server/src/main.rs b/dora-language-server/src/main.rs
@@ -306,7 +306,6 @@ fn compile_project(project: ProjectConfig, sender: Sender<MainLoopTask>) {
         program_file: Some(FileContent::Path(project.main.clone())),
         packages: Vec::new(),
         boots: false,
-        new_exhaustiveness: false,
     };
 
     let mut sa = Sema::new(sem_args);

diff --git a/dora-sema-fuzzer/src/main.rs b/dora-sema-fuzzer/src/main.rs
@@ -16,7 +16,6 @@ fn check_program(program: String) {
         program_file: Some(FileContent::Content(program)),
         packages: Vec::new(),
         boots: false,
-        new_exhaustiveness: false,
     };
 
     let mut sa = Sema::new(sem_args);

diff --git a/dora/src/driver/flags.rs b/dora/src/driver/flags.rs
@@ -437,7 +437,6 @@ pub fn create_sema_flags(flags: &DriverFlags, program_file: PathBuf) -> SemaFlag
         program_file: Some(FileContent::Path(program_file)),
         packages,
         boots: flags.include_boots(),
-        new_exhaustiveness: false,
     }
 }