Work on ArrayChecker

audulus · Sep 29, 2023 · b8d1d90 · b8d1d90
1 parent fcf321f
commit b8d1d90
Showing 1 changed file with 48 additions and 29 deletions.
diff --git a/src/array_checker.rs b/src/array_checker.rs
@@ -50,6 +50,42 @@ impl ArrayChecker {
         }
     }
 
+    fn match_expr(&mut self, expr: ExprID, decl: &FuncDecl, decls: &DeclTable) -> Option<IndexConstraint> {
+
+        // Simplest form: match expressions of the form i < n, where n is an integer literal
+        if let Expr::Binop(Binop::Less, lhs, rhs) = &decl.arena[expr] {
+            if let Expr::Id(name) = &decl.arena[*lhs] {
+                if let Expr::Int(n) = &decl.arena[*rhs] {
+                    self.constraints.push(IndexConstraint {
+                        name: *name,
+                        max: Some(*n),
+                        min: None,
+                    })
+                }
+            }
+        }
+
+        // match expressions of the form i < id, where id is another variable
+        // with a constraint
+        if let Expr::Binop(Binop::Less, lhs, rhs) = &decl.arena[expr] {
+            if let Expr::Id(name) = &decl.arena[*lhs] {
+                if let Expr::Id(max_name) = &decl.arena[*rhs] {
+                    if let Some(c) = self.constraints.iter().find(|c| c.name == *max_name) {
+                        if let Some(max) = c.max {
+                            self.constraints.push(IndexConstraint {
+                                name: *name,
+                                max: Some(max),
+                                min: None,
+                            })
+                        }
+                    }
+                }
+            }
+        }
+
+        None
+    }
+
     fn check_expr(&mut self, expr: ExprID, decl: &FuncDecl, decls: &DeclTable) -> IndexInterval {
         match &decl.arena[expr] {
             Expr::Int(x) => {
@@ -91,35 +127,8 @@ impl ArrayChecker {
 
                 self.check_expr(*cond, decl, decls);
 
-                // Simplest form: match expressions of the form i < n, where n is an integer literal
-                if let Expr::Binop(Binop::Less, lhs, rhs) = &decl.arena[*cond] {
-                    if let Expr::Id(name) = &decl.arena[*lhs] {
-                        if let Expr::Int(n) = &decl.arena[*rhs] {
-                            self.constraints.push(IndexConstraint {
-                                name: *name,
-                                max: Some(*n),
-                                min: None,
-                            })
-                        }
-                    }
-                }
-
-                // match expressions of the form i < id, where id is another variable
-                // with a constraint
-                if let Expr::Binop(Binop::Less, lhs, rhs) = &decl.arena[*cond] {
-                    if let Expr::Id(name) = &decl.arena[*lhs] {
-                        if let Expr::Id(max_name) = &decl.arena[*rhs] {
-                            if let Some(c) = self.constraints.iter().find(|c| c.name == *max_name) {
-                                if let Some(max) = c.max {
-                                    self.constraints.push(IndexConstraint {
-                                        name: *name,
-                                        max: Some(max),
-                                        min: None,
-                                    })
-                                }
-                            }
-                        }
-                    }
+                if let Some(constraint) = self.match_expr(*cond, decl, decls) {
+                    self.constraints.push(constraint)
                 }
 
                 let mut r = self.check_expr(*then_expr, decl, decls);
@@ -160,6 +169,16 @@ impl ArrayChecker {
 
                 IndexInterval::default()
             }
+            Expr::While(cond, body) => {
+
+                if let Some(constraint) = self.match_expr(*cond, decl, decls) {
+                    self.constraints.push(constraint)
+                }
+
+                self.check_expr(*body, decl, decls);
+
+                IndexInterval::default()
+            }
             _ => {
                 IndexInterval::default()
             }